:: EQREL_1 semantic presentation
:: Showing IDV graph ... (Click the Palm Trees again to close it)
:: deftheorem defines nabla EQREL_1:def 1 :
Lm1:
for i, j being Nat st i < j holds
j - i is Nat
by NAT_1:61;
theorem :: EQREL_1:1
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: EQREL_1:2
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: EQREL_1:3
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: EQREL_1:4
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:5
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: EQREL_1:6
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th7: :: EQREL_1:7
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm2:
for x, y, X being set
for R being Relation of X st [x,y] in R holds
( x in X & y in X )
theorem :: EQREL_1:8
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: EQREL_1:9
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: EQREL_1:10
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th11: :: EQREL_1:11
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th12: :: EQREL_1:12
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th13: :: EQREL_1:13
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:14
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:15
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th16: :: EQREL_1:16
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:17
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:18
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th19: :: EQREL_1:19
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th20: :: EQREL_1:20
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem EQREL_1:def 2 :
canceled;
:: deftheorem Def3 defines "\/" EQREL_1:def 3 :
theorem :: EQREL_1:21
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem :: EQREL_1:22
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:23
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:24
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:25
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
scheme :: EQREL_1:sch 1
ExEqRel{
F1()
-> set ,
P1[
set ,
set ] } :
provided
A1:
for
x being
set st
x in F1() holds
P1[
x,
x]
and A2:
for
x,
y being
set st
P1[
x,
y] holds
P1[
y,
x]
and A3:
for
x,
y,
z being
set st
P1[
x,
y] &
P1[
y,
z] holds
P1[
x,
z]
:: deftheorem defines Class EQREL_1:def 4 :
theorem :: EQREL_1:26
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th27: :: EQREL_1:27
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th28: :: EQREL_1:28
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:29
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:30
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
Lm3:
for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( [x,y] in EqR iff Class EqR,x = Class EqR,y )
theorem Th31: :: EQREL_1:31
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th32: :: EQREL_1:32
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:33
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th34: :: EQREL_1:34
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th35: :: EQREL_1:35
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:36
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem Th37: :: EQREL_1:37
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:38
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def5 defines Class EQREL_1:def 5 :
theorem :: EQREL_1:39
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th40: :: EQREL_1:40
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
:: deftheorem Def6 defines a_partition EQREL_1:def 6 :
theorem :: EQREL_1:41
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
canceled;
theorem Th42: :: EQREL_1:42
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:43
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:44
:: Showing IDV graph ... (Click the Palm Tree again to close it) 
theorem :: EQREL_1:45
:: Showing IDV graph ... (Click the Palm Tree again to close it) 