:: EQREL_1 semantic presentation

begin


definition
let X be set ;
func nabla X ->  Relation of X equals :: EQREL_1:def 1
[:X,X:];
coherence
 [:X,X:] is Relation of X
proof
 [:X,X:] c= [:X,X:] ;
hence  [:X,X:] is Relation of X ; ::_thesis: verum
end;
end;

:: deftheorem  defines nabla EQREL_1:def_1_:_
 for X being set holds nabla X = [:X,X:];

registration
let X be set ;
cluster nabla X ->  reflexive total ;
coherence
 ( nabla X is total & nabla X is reflexive )
proof
thus  dom (nabla X) c= X ; :: according to XBOOLE_0:def_10,PARTFUN1:def_2 ::_thesis: ( X c= dom (nabla X) & nabla X is reflexive )
thus  X c= dom (nabla X) ::_thesis: nabla X is reflexive
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in X or x in dom (nabla X) )
assume  x in X ; ::_thesis: x in dom (nabla X)
then  [x,x] in [:X,X:] by ZFMISC_1:87;
hence  x in dom (nabla X) by XTUPLE_0:def_12; ::_thesis: verum
end;
let x be set ; :: according to RELAT_2:def_1,RELAT_2:def_9 ::_thesis: ( not x in field (nabla X) or [x,x] in nabla X )
assume  x in field (nabla X) ; ::_thesis: [x,x] in nabla X
then  x in (dom (nabla X)) \/ (rng (nabla X)) ;
hence  [x,x] in nabla X by ZFMISC_1:87; ::_thesis: verum
end;
end;

definition
let X be set ;
let R1, R2 be Relation of X;
:: original: /\
redefine funcR1 /\ R2 ->  Relation of X;
coherence
 R1 /\ R2 is Relation of X
proof
 R1 /\ R2 c= [:X,X:] ;
hence  R1 /\ R2 is Relation of X ; ::_thesis: verum
end;
:: original: \/
redefine funcR1 \/ R2 ->  Relation of X;
coherence
 R1 \/ R2 is Relation of X
proof
 R1 \/ R2 c= [:X,X:] ;
hence  R1 \/ R2 is Relation of X ; ::_thesis: verum
end;
end;

theorem :: EQREL_1:1
for X being set
for R1 being Relation of X holds (nabla X) \/ R1 = nabla X by XBOOLE_1:12;

theorem :: EQREL_1:2
for X being set holds
( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X )
proof
let X be set ; ::_thesis: ( id X is_reflexive_in X & id X is_symmetric_in X & id X is_transitive_in X )
thus  for x being set st x in X holds
[x,x] in id X by RELAT_1:def_10; :: according to RELAT_2:def_1 ::_thesis: ( id X is_symmetric_in X & id X is_transitive_in X )
thus  for x, y being set st x in X & y in X & [x,y] in id X holds
[y,x] in id X by RELAT_1:def_10; :: according to RELAT_2:def_3 ::_thesis: id X is_transitive_in X
thus  for x, y, z being set st x in X & y in X & z in X & [x,y] in id X & [y,z] in id X holds
[x,z] in id X by RELAT_1:def_10; :: according to RELAT_2:def_8 ::_thesis: verum
end;

definition
let X be set ;
mode Tolerance of X is reflexive symmetric total Relation of X;
mode Equivalence_Relation of X is symmetric transitive total Relation of X;
end;

theorem :: EQREL_1:3
for X being set holds id X is Equivalence_Relation of X ;

theorem Th4: :: EQREL_1:4
for X being set holds nabla X is Equivalence_Relation of X
proof
let X be set ; ::_thesis: nabla X is Equivalence_Relation of X
 for x, y being set st x in X & y in X & [x,y] in nabla X holds
[y,x] in nabla X by ZFMISC_1:88;
then A1: nabla X is_symmetric_in X by RELAT_2:def_3;
 for x, y, z being set st x in X & y in X & z in X & [x,y] in nabla X & [y,z] in nabla X holds
[x,z] in nabla X by ZFMISC_1:87;
then A2: nabla X is_transitive_in X by RELAT_2:def_8;
 field (nabla X) = X by ORDERS_1:12;
hence  nabla X is Equivalence_Relation of X by A1, A2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;

registration
let X be set ;
cluster nabla X ->  symmetric transitive total ;
coherence
 ( nabla X is total & nabla X is symmetric & nabla X is transitive ) by Th4;
end;

    Lm1:  for x, y, X being set
for R being Relation of X st [x,y] in R holds
( x in X & y in X )
proof
let x, y, X be set ; ::_thesis: for R being Relation of X st [x,y] in R holds
( x in X & y in X )
let R be Relation of X; ::_thesis: ( [x,y] in R implies ( x in X & y in X ) )
assume  [x,y] in R ; ::_thesis: ( x in X & y in X )
then  ( x in dom R & y in rng R ) by XTUPLE_0:def_12, XTUPLE_0:def_13;
hence  ( x in X & y in X ) ; ::_thesis: verum
end;

theorem Th5: :: EQREL_1:5
for X, x being set
for R being reflexive total Relation of X st x in X holds
[x,x] in R
proof
let X, x be set ; ::_thesis: for R being reflexive total Relation of X st x in X holds
[x,x] in R
let R be reflexive total Relation of X; ::_thesis: ( x in X implies [x,x] in R )
 field R = X by ORDERS_1:12;
then  R is_reflexive_in X by RELAT_2:def_9;
hence  ( x in X implies [x,x] in R ) by RELAT_2:def_1; ::_thesis: verum
end;

theorem Th6: :: EQREL_1:6
for X, x, y being set
for R being symmetric total Relation of X st [x,y] in R holds
[y,x] in R
proof
let X, x, y be set ; ::_thesis: for R being symmetric total Relation of X st [x,y] in R holds
[y,x] in R
let R be symmetric total Relation of X; ::_thesis: ( [x,y] in R implies [y,x] in R )
 field R = X by ORDERS_1:12;
then A1: R is_symmetric_in X by RELAT_2:def_11;
assume A2: [x,y] in R ; ::_thesis: [y,x] in R
then  ( x in X & y in X ) by Lm1;
hence  [y,x] in R by A2, A1, RELAT_2:def_3; ::_thesis: verum
end;

theorem Th7: :: EQREL_1:7
for X, x, y, z being set
for R being transitive total Relation of X st [x,y] in R & [y,z] in R holds
[x,z] in R
proof
let X, x, y, z be set ; ::_thesis: for R being transitive total Relation of X st [x,y] in R & [y,z] in R holds
[x,z] in R
let R be transitive total Relation of X; ::_thesis: ( [x,y] in R & [y,z] in R implies [x,z] in R )
assume that
A1: [x,y] in R and
A2: [y,z] in R ; ::_thesis: [x,z] in R
A3: z in X by A2, Lm1;
 field R = X by ORDERS_1:12;
then A4: R is_transitive_in X by RELAT_2:def_16;
 ( x in X & y in X ) by A1, Lm1;
hence  [x,z] in R by A1, A2, A3, A4, RELAT_2:def_8; ::_thesis: verum
end;

theorem :: EQREL_1:8
for X being set
for R being reflexive total Relation of X st ex x being set st x in X holds
R <> {} ;

theorem Th9: :: EQREL_1:9
for X being set
for R being Relation of X holds
( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )
proof
let X be set ; ::_thesis: for R being Relation of X holds
( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )
let R be Relation of X; ::_thesis: ( R is Equivalence_Relation of X iff ( R is reflexive & R is symmetric & R is transitive & field R = X ) )
thus  ( R is Equivalence_Relation of X implies ( R is reflexive & R is symmetric & R is transitive & field R = X ) ) by ORDERS_1:12; ::_thesis: ( R is reflexive & R is symmetric & R is transitive & field R = X implies R is Equivalence_Relation of X )
assume that
A1: R is reflexive and
A2: ( R is symmetric & R is transitive ) and
A3: field R = X ; ::_thesis: R is Equivalence_Relation of X
 R is_reflexive_in X by A1, A3, RELAT_2:def_9;
then  dom R = X by ORDERS_1:13;
hence  R is Equivalence_Relation of X by A2, PARTFUN1:def_2; ::_thesis: verum
end;

definition
let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
:: original: /\
redefine funcEqR1 /\ EqR2 ->  Equivalence_Relation of X;
coherence
 EqR1 /\ EqR2 is Equivalence_Relation of X
proof
 for x being set st x in X holds
[x,x] in EqR2 by Th5;
then A1: id X c= EqR2 by RELAT_1:47;
 for x being set st x in X holds
[x,x] in EqR1 by Th5;
then  id X c= EqR1 by RELAT_1:47;
then  id X c= EqR1 /\ EqR2 by A1, XBOOLE_1:19;
then  ( dom (EqR1 /\ EqR2) = X & rng (EqR1 /\ EqR2) = X ) by RELSET_1:16, RELSET_1:17;
then  field (EqR1 /\ EqR2) = X ;
hence  EqR1 /\ EqR2 is Equivalence_Relation of X by Th9; ::_thesis: verum
end;
end;

theorem :: EQREL_1:10
for X being set
for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X holds (id X) /\ EqR = id X
let EqR be Equivalence_Relation of X; ::_thesis: (id X) /\ EqR = id X
now__::_thesis:_for_x,_y_being_set_st_[x,y]_in_id_X_holds_
[x,y]_in_EqR
let x, y be set ; ::_thesis: ( [x,y] in id X implies [x,y] in EqR )
assume  [x,y] in id X ; ::_thesis: [x,y] in EqR
then  ( x in X & x = y ) by RELAT_1:def_10;
hence  [x,y] in EqR by Th5; ::_thesis: verum
end;
then  id X c= EqR by RELAT_1:def_3;
hence  (id X) /\ EqR = id X by XBOOLE_1:28; ::_thesis: verum
end;

theorem Th11: :: EQREL_1:11
for X being set
for SFXX being Subset-Family of [:X,X:] st SFXX <> {} & ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) holds
meet SFXX is Equivalence_Relation of X
proof
let X be set ; ::_thesis: for SFXX being Subset-Family of [:X,X:] st SFXX <> {} & ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) holds
meet SFXX is Equivalence_Relation of X
let SFXX be Subset-Family of [:X,X:]; ::_thesis: ( SFXX <> {} & ( for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ) implies meet SFXX is Equivalence_Relation of X )
assume that
A1: SFXX <> {} and
A2: for Y being set st Y in SFXX holds
Y is Equivalence_Relation of X ; ::_thesis: meet SFXX is Equivalence_Relation of X
reconsider XX = meet SFXX as Relation of X ;
A3: XX is_symmetric_in X
proof
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in XX or [b1,x] in XX )
let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in XX or [y,x] in XX )
assume that
 x in X and
 y in X and
A4: [x,y] in XX ; ::_thesis: [y,x] in XX
now__::_thesis:_for_Y_being_set_st_Y_in_SFXX_holds_
[y,x]_in_Y
let Y be set ; ::_thesis: ( Y in SFXX implies [y,x] in Y )
assume  Y in SFXX ; ::_thesis: [y,x] in Y
then  ( Y is Equivalence_Relation of X & [x,y] in Y ) by A2, A4, SETFAM_1:def_1;
hence  [y,x] in Y by Th6; ::_thesis: verum
end;
hence  [y,x] in XX by A1, SETFAM_1:def_1; ::_thesis: verum
end;
A5: XX is_transitive_in X
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in XX or not [b1,b2] in XX or [x,b2] in XX )
let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in XX or not [y,z] in XX or [x,z] in XX )
assume that
 x in X and
 y in X and
 z in X and
A6: [x,y] in XX and
A7: [y,z] in XX ; ::_thesis: [x,z] in XX
now__::_thesis:_for_Y_being_set_st_Y_in_SFXX_holds_
[x,z]_in_Y
let Y be set ; ::_thesis: ( Y in SFXX implies [x,z] in Y )
assume A8: Y in SFXX ; ::_thesis: [x,z] in Y
then A9: [y,z] in Y by A7, SETFAM_1:def_1;
 ( Y is Equivalence_Relation of X & [x,y] in Y ) by A2, A6, A8, SETFAM_1:def_1;
hence  [x,z] in Y by A9, Th7; ::_thesis: verum
end;
hence  [x,z] in XX by A1, SETFAM_1:def_1; ::_thesis: verum
end;
 XX is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in XX )
assume A10: x in X ; ::_thesis: [x,x] in XX
 for Y being set st Y in SFXX holds
[x,x] in Y
proof
let Y be set ; ::_thesis: ( Y in SFXX implies [x,x] in Y )
assume  Y in SFXX ; ::_thesis: [x,x] in Y
then  Y is Equivalence_Relation of X by A2;
hence  [x,x] in Y by A10, Th5; ::_thesis: verum
end;
hence  [x,x] in XX by A1, SETFAM_1:def_1; ::_thesis: verum
end;
then  ( field XX = X & dom XX = X ) by ORDERS_1:13;
hence  meet SFXX is Equivalence_Relation of X by A3, A5, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16; ::_thesis: verum
end;

theorem Th12: :: EQREL_1:12
for X being set
for R being Relation of X ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
proof
let X be set ; ::_thesis: for R being Relation of X ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
let R be Relation of X; ::_thesis: ex EqR being Equivalence_Relation of X st
( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
defpred S1[ set ] means ( $1 is Equivalence_Relation of X & R c= $1 );
consider F being Subset-Family of [:X,X:] such that
A1: for AX being Subset of [:X,X:] holds
( AX in F iff S1[AX] ) from SUBSET_1:sch_3();
 R c= nabla X ;
then A2: F <> {} by A1;
 for Y being set st Y in F holds
Y is Equivalence_Relation of X by A1;
then reconsider EqR = meet F as Equivalence_Relation of X by A2, Th11;
A3: now__::_thesis:_for_EqR2_being_Equivalence_Relation_of_X_st_R_c=_EqR2_holds_
EqR_c=_EqR2
let EqR2 be Equivalence_Relation of X; ::_thesis: ( R c= EqR2 implies EqR c= EqR2 )
assume  R c= EqR2 ; ::_thesis: EqR c= EqR2
then  EqR2 in F by A1;
hence  EqR c= EqR2 by SETFAM_1:3; ::_thesis: verum
end;
take  EqR ; ::_thesis: ( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) )
 for Y being set st Y in F holds
R c= Y by A1;
hence  ( R c= EqR & ( for EqR2 being Equivalence_Relation of X st R c= EqR2 holds
EqR c= EqR2 ) ) by A2, A3, SETFAM_1:5; ::_thesis: verum
end;

definition
let X be set ;
let EqR1, EqR2 be Equivalence_Relation of X;
funcEqR1 "\/" EqR2 ->  Equivalence_Relation of X means :Def2: :: EQREL_1:def 2
( EqR1 \/ EqR2 c= it & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
it c= EqR ) );
existence
 ex b1 being Equivalence_Relation of X st
( EqR1 \/ EqR2 c= b1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) ) by Th12;
uniqueness
 for b1, b2 being Equivalence_Relation of X st EqR1 \/ EqR2 c= b1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) & EqR1 \/ EqR2 c= b2 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b2 c= EqR ) holds
b1 = b2
proof
let R1, R2 be Equivalence_Relation of X; ::_thesis: ( EqR1 \/ EqR2 c= R1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R1 c= EqR ) & EqR1 \/ EqR2 c= R2 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R2 c= EqR ) implies R1 = R2 )
assume  ( EqR1 \/ EqR2 c= R1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R1 c= EqR ) & EqR1 \/ EqR2 c= R2 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
R2 c= EqR ) ) ; ::_thesis: R1 = R2
then  ( R1 c= R2 & R2 c= R1 ) ;
hence  R1 = R2 by XBOOLE_0:def_10; ::_thesis: verum
end;
commutativity
 for b1, EqR1, EqR2 being Equivalence_Relation of X st EqR1 \/ EqR2 c= b1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b1 c= EqR ) holds
( EqR2 \/ EqR1 c= b1 & ( for EqR being Equivalence_Relation of X st EqR2 \/ EqR1 c= EqR holds
b1 c= EqR ) ) ;
idempotence
 for EqR1 being Equivalence_Relation of X holds
( EqR1 \/ EqR1 c= EqR1 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR1 c= EqR holds
EqR1 c= EqR ) ) ;
end;

:: deftheorem Def2 defines "\/" EQREL_1:def_2_:_
 for X being set
for EqR1, EqR2, b4 being Equivalence_Relation of X holds
( b4 = EqR1 "\/" EqR2 iff ( EqR1 \/ EqR2 c= b4 & ( for EqR being Equivalence_Relation of X st EqR1 \/ EqR2 c= EqR holds
b4 c= EqR ) ) );

theorem :: EQREL_1:13
for X being set
for EqR1, EqR2, EqR3 being Equivalence_Relation of X holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
proof
let X be set ; ::_thesis: for EqR1, EqR2, EqR3 being Equivalence_Relation of X holds (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
let EqR1, EqR2, EqR3 be Equivalence_Relation of X; ::_thesis: (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3)
 for EqR4 being Equivalence_Relation of X st EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) holds
(EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
proof
let EqR4 be Equivalence_Relation of X; ::_thesis: ( EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) implies (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 )
A1: EqR2 \/ EqR3 c= EqR2 "\/" EqR3 by Def2;
assume  EqR4 = EqR1 "\/" (EqR2 "\/" EqR3) ; ::_thesis: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4
then A2: EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by Def2;
 EqR2 "\/" EqR3 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
then  EqR2 "\/" EqR3 c= EqR4 by A2, XBOOLE_1:1;
then A3: EqR2 \/ EqR3 c= EqR4 by A1, XBOOLE_1:1;
 EqR2 c= EqR2 \/ EqR3 by XBOOLE_1:7;
then A4: EqR2 c= EqR4 by A3, XBOOLE_1:1;
 EqR1 c= EqR1 \/ (EqR2 "\/" EqR3) by XBOOLE_1:7;
then  EqR1 c= EqR4 by A2, XBOOLE_1:1;
then  EqR1 \/ EqR2 c= EqR4 by A4, XBOOLE_1:8;
then A5: EqR1 "\/" EqR2 c= EqR4 by Def2;
 EqR3 c= EqR2 \/ EqR3 by XBOOLE_1:7;
then  EqR3 c= EqR4 by A3, XBOOLE_1:1;
then  (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by A5, XBOOLE_1:8;
hence  (EqR1 "\/" EqR2) "\/" EqR3 c= EqR4 by Def2; ::_thesis: verum
end;
then A6: (EqR1 "\/" EqR2) "\/" EqR3 c= EqR1 "\/" (EqR2 "\/" EqR3) ;
 for EqR4 being Equivalence_Relation of X st EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 holds
EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
proof
let EqR4 be Equivalence_Relation of X; ::_thesis: ( EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 implies EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 )
A7: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
assume  EqR4 = (EqR1 "\/" EqR2) "\/" EqR3 ; ::_thesis: EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4
then A8: (EqR1 "\/" EqR2) \/ EqR3 c= EqR4 by Def2;
 EqR1 "\/" EqR2 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
then  EqR1 "\/" EqR2 c= EqR4 by A8, XBOOLE_1:1;
then A9: EqR1 \/ EqR2 c= EqR4 by A7, XBOOLE_1:1;
 EqR3 c= (EqR1 "\/" EqR2) \/ EqR3 by XBOOLE_1:7;
then A10: EqR3 c= EqR4 by A8, XBOOLE_1:1;
 EqR2 c= EqR1 \/ EqR2 by XBOOLE_1:7;
then  EqR2 c= EqR4 by A9, XBOOLE_1:1;
then  EqR2 \/ EqR3 c= EqR4 by A10, XBOOLE_1:8;
then A11: EqR2 "\/" EqR3 c= EqR4 by Def2;
 EqR1 c= EqR1 \/ EqR2 by XBOOLE_1:7;
then  EqR1 c= EqR4 by A9, XBOOLE_1:1;
then  EqR1 \/ (EqR2 "\/" EqR3) c= EqR4 by A11, XBOOLE_1:8;
hence  EqR1 "\/" (EqR2 "\/" EqR3) c= EqR4 by Def2; ::_thesis: verum
end;
then  EqR1 "\/" (EqR2 "\/" EqR3) c= (EqR1 "\/" EqR2) "\/" EqR3 ;
hence  (EqR1 "\/" EqR2) "\/" EqR3 = EqR1 "\/" (EqR2 "\/" EqR3) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: EQREL_1:14
for X being set
for EqR being Equivalence_Relation of X holds EqR "\/" EqR = EqR ;

theorem :: EQREL_1:15
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" EqR2 = EqR2 "\/" EqR1 ;

theorem :: EQREL_1:16
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
proof
let X be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 /\ (EqR1 "\/" EqR2) = EqR1
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: EqR1 /\ (EqR1 "\/" EqR2) = EqR1
thus  EqR1 /\ (EqR1 "\/" EqR2) c= EqR1 by XBOOLE_1:17; :: according to XBOOLE_0:def_10 ::_thesis: EqR1 c= EqR1 /\ (EqR1 "\/" EqR2)
 ( EqR1 c= EqR1 \/ EqR2 & EqR1 \/ EqR2 c= EqR1 "\/" EqR2 ) by Def2, XBOOLE_1:7;
then  EqR1 c= EqR1 "\/" EqR2 by XBOOLE_1:1;
hence  EqR1 c= EqR1 /\ (EqR1 "\/" EqR2) by XBOOLE_1:19; ::_thesis: verum
end;

theorem :: EQREL_1:17
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" (EqR1 /\ EqR2) = EqR1
proof
let X be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X holds EqR1 "\/" (EqR1 /\ EqR2) = EqR1
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: EqR1 "\/" (EqR1 /\ EqR2) = EqR1
 ( EqR1 = EqR1 \/ (EqR1 /\ EqR2) & ( for EqR being Equivalence_Relation of X st EqR1 \/ (EqR1 /\ EqR2) c= EqR holds
EqR1 c= EqR ) ) by XBOOLE_1:22;
hence  EqR1 "\/" (EqR1 /\ EqR2) = EqR1 by Def2; ::_thesis: verum
end;

scheme :: EQREL_1:sch 1
ExEqRel{ F1() ->  set , P1[ set , set ] } :
 ex EqR being Equivalence_Relation of F1() st
for x, y being set holds
( [x,y] in EqR iff ( x in F1() & y in F1() & P1[x,y] ) )
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]
proof
consider Y being Relation of F1(),F1() such that
A4: for x, y being set holds
( [x,y] in Y iff ( x in F1() & y in F1() & P1[x,y] ) ) from RELSET_1:sch_1();
A5: Y is_transitive_in F1()
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in F1() or not b1 in F1() or not b2 in F1() or not [x,b1] in Y or not [b1,b2] in Y or [x,b2] in Y )
let y, z be set ; ::_thesis: ( not x in F1() or not y in F1() or not z in F1() or not [x,y] in Y or not [y,z] in Y or [x,z] in Y )
assume that
A6: x in F1() and
 y in F1() and
A7: z in F1() and
A8: ( [x,y] in Y & [y,z] in Y ) ; ::_thesis: [x,z] in Y
 ( P1[x,y] & P1[y,z] ) by A4, A8;
then  P1[x,z] by A3;
hence  [x,z] in Y by A4, A6, A7; ::_thesis: verum
end;
A9: Y is_symmetric_in F1()
proof
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in F1() or not b1 in F1() or not [x,b1] in Y or [b1,x] in Y )
let y be set ; ::_thesis: ( not x in F1() or not y in F1() or not [x,y] in Y or [y,x] in Y )
assume that
A10: ( x in F1() & y in F1() ) and
A11: [x,y] in Y ; ::_thesis: [y,x] in Y
 P1[x,y] by A4, A11;
then  P1[y,x] by A2;
hence  [y,x] in Y by A4, A10; ::_thesis: verum
end;
 Y is_reflexive_in F1()
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in F1() or [x,x] in Y )
assume A12: x in F1() ; ::_thesis: [x,x] in Y
then  P1[x,x] by A1;
hence  [x,x] in Y by A4, A12; ::_thesis: verum
end;
then  ( field Y = F1() & dom Y = F1() ) by ORDERS_1:13;
then reconsider R1 = Y as Equivalence_Relation of F1() by A9, A5, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16;
take  R1 ; ::_thesis: for x, y being set holds
( [x,y] in R1 iff ( x in F1() & y in F1() & P1[x,y] ) )
thus  for x, y being set holds
( [x,y] in R1 iff ( x in F1() & y in F1() & P1[x,y] ) ) by A4; ::_thesis: verum
end;

notation
let R be Relation;
let x be set ;
synonym  Class (R,x) for  Im (R,x);
end;

definition
let X, Y be set ;
let R be Relation of X,Y;
let x be set ;
:: original: Class
redefine func Class (R,x) ->  Subset of Y;
coherence
 Class (R,x) is Subset of Y
proof
 R .: {x} c= Y ;
hence  Class (R,x) is Subset of Y ; ::_thesis: verum
end;
end;

theorem :: EQREL_1:18
for y, x being set
for R being Relation holds
( y in Class (R,x) iff [x,y] in R )
proof
let y, x be set ; ::_thesis: for R being Relation holds
( y in Class (R,x) iff [x,y] in R )
let R be Relation; ::_thesis: ( y in Class (R,x) iff [x,y] in R )
thus  ( y in Class (R,x) implies [x,y] in R ) ::_thesis: ( [x,y] in R implies y in Class (R,x) )
proof
assume  y in Class (R,x) ; ::_thesis: [x,y] in R
then  ex z being set st
( [z,y] in R & z in {x} ) by RELAT_1:def_13;
hence  [x,y] in R by TARSKI:def_1; ::_thesis: verum
end;
A1: x in {x} by TARSKI:def_1;
assume  [x,y] in R ; ::_thesis: y in Class (R,x)
hence  y in Class (R,x) by A1, RELAT_1:def_13; ::_thesis: verum
end;

theorem Th19: :: EQREL_1:19
for X, y, x being set
for R being symmetric total Relation of X holds
( y in Class (R,x) iff [y,x] in R )
proof
let X, y, x be set ; ::_thesis: for R being symmetric total Relation of X holds
( y in Class (R,x) iff [y,x] in R )
let R be symmetric total Relation of X; ::_thesis: ( y in Class (R,x) iff [y,x] in R )
thus  ( y in Class (R,x) implies [y,x] in R ) ::_thesis: ( [y,x] in R implies y in Class (R,x) )
proof
assume  y in Class (R,x) ; ::_thesis: [y,x] in R
then  ex z being set st
( [z,y] in R & z in {x} ) by RELAT_1:def_13;
then  [x,y] in R by TARSKI:def_1;
hence  [y,x] in R by Th6; ::_thesis: verum
end;
assume  [y,x] in R ; ::_thesis: y in Class (R,x)
then A1: [x,y] in R by Th6;
 x in {x} by TARSKI:def_1;
hence  y in Class (R,x) by A1, RELAT_1:def_13; ::_thesis: verum
end;

theorem Th20: :: EQREL_1:20
for X being set
for R being Tolerance of X
for x being set st x in X holds
x in Class (R,x)
proof
let X be set ; ::_thesis: for R being Tolerance of X
for x being set st x in X holds
x in Class (R,x)
let R be Tolerance of X; ::_thesis: for x being set st x in X holds
x in Class (R,x)
let x be set ; ::_thesis: ( x in X implies x in Class (R,x) )
assume  x in X ; ::_thesis: x in Class (R,x)
then  [x,x] in R by Th5;
hence  x in Class (R,x) by Th19; ::_thesis: verum
end;

theorem :: EQREL_1:21
for X being set
for R being Tolerance of X
for x being set st x in X holds
ex y being set st x in Class (R,y)
proof
let X be set ; ::_thesis: for R being Tolerance of X
for x being set st x in X holds
ex y being set st x in Class (R,y)
let R be Tolerance of X; ::_thesis: for x being set st x in X holds
ex y being set st x in Class (R,y)
let x be set ; ::_thesis: ( x in X implies ex y being set st x in Class (R,y) )
assume  x in X ; ::_thesis: ex y being set st x in Class (R,y)
then  x in Class (R,x) by Th20;
hence  ex y being set st x in Class (R,y) ; ::_thesis: verum
end;

theorem :: EQREL_1:22
for X, y, x, z being set
for R being transitive Tolerance of X st y in Class (R,x) & z in Class (R,x) holds
[y,z] in R
proof
let X, y, x, z be set ; ::_thesis: for R being transitive Tolerance of X st y in Class (R,x) & z in Class (R,x) holds
[y,z] in R
let R be transitive Tolerance of X; ::_thesis: ( y in Class (R,x) & z in Class (R,x) implies [y,z] in R )
assume that
A1: y in Class (R,x) and
A2: z in Class (R,x) ; ::_thesis: [y,z] in R
 [z,x] in R by A2, Th19;
then A3: [x,z] in R by Th6;
 [y,x] in R by A1, Th19;
hence  [y,z] in R by A3, Th7; ::_thesis: verum
end;

Lm2:  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) )
proof
let X, y be set ; ::_thesis: 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) )
let EqR be Equivalence_Relation of X; ::_thesis: for x being set st x in X holds
( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )
let x be set ; ::_thesis: ( x in X implies ( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) ) )
assume A1: x in X ; ::_thesis: ( [x,y] in EqR iff Class (EqR,x) = Class (EqR,y) )
thus  ( [x,y] in EqR implies Class (EqR,x) = Class (EqR,y) ) ::_thesis: ( Class (EqR,x) = Class (EqR,y) implies [x,y] in EqR )
proof
assume A2: [x,y] in EqR ; ::_thesis: Class (EqR,x) = Class (EqR,y)
now__::_thesis:_for_z_being_set_st_z_in_Class_(EqR,y)_holds_
z_in_Class_(EqR,x)
let z be set ; ::_thesis: ( z in Class (EqR,y) implies z in Class (EqR,x) )
assume  z in Class (EqR,y) ; ::_thesis: z in Class (EqR,x)
then A3: [z,y] in EqR by Th19;
 [y,x] in EqR by A2, Th6;
then  [z,x] in EqR by A3, Th7;
hence  z in Class (EqR,x) by Th19; ::_thesis: verum
end;
then A4: Class (EqR,y) c= Class (EqR,x) by TARSKI:def_3;
now__::_thesis:_for_z_being_set_st_z_in_Class_(EqR,x)_holds_
z_in_Class_(EqR,y)
let z be set ; ::_thesis: ( z in Class (EqR,x) implies z in Class (EqR,y) )
assume  z in Class (EqR,x) ; ::_thesis: z in Class (EqR,y)
then  [z,x] in EqR by Th19;
then  [z,y] in EqR by A2, Th7;
hence  z in Class (EqR,y) by Th19; ::_thesis: verum
end;
then  Class (EqR,x) c= Class (EqR,y) by TARSKI:def_3;
hence  Class (EqR,x) = Class (EqR,y) by A4, XBOOLE_0:def_10; ::_thesis: verum
end;
assume  Class (EqR,x) = Class (EqR,y) ; ::_thesis: [x,y] in EqR
then  x in Class (EqR,y) by A1, Th20;
hence  [x,y] in EqR by Th19; ::_thesis: verum
end;

theorem Th23: :: EQREL_1:23
for X, y being set
for EqR being Equivalence_Relation of X
for x being set st x in X holds
( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
proof
let X, y be set ; ::_thesis: for EqR being Equivalence_Relation of X
for x being set st x in X holds
( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
let EqR be Equivalence_Relation of X; ::_thesis: for x being set st x in X holds
( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
let x be set ; ::_thesis: ( x in X implies ( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) ) )
assume A1: x in X ; ::_thesis: ( y in Class (EqR,x) iff Class (EqR,x) = Class (EqR,y) )
thus  ( y in Class (EqR,x) implies Class (EqR,x) = Class (EqR,y) ) ::_thesis: ( Class (EqR,x) = Class (EqR,y) implies y in Class (EqR,x) )
proof
assume  y in Class (EqR,x) ; ::_thesis: Class (EqR,x) = Class (EqR,y)
then  [y,x] in EqR by Th19;
then  [x,y] in EqR by Th6;
hence  Class (EqR,x) = Class (EqR,y) by A1, Lm2; ::_thesis: verum
end;
assume  Class (EqR,x) = Class (EqR,y) ; ::_thesis: y in Class (EqR,x)
then  [x,y] in EqR by A1, Lm2;
then  [y,x] in EqR by Th6;
hence  y in Class (EqR,x) by Th19; ::_thesis: verum
end;

theorem Th24: :: EQREL_1:24
for X being set
for EqR being Equivalence_Relation of X
for x, y being set holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X
for x, y being set holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
let EqR be Equivalence_Relation of X; ::_thesis: for x, y being set holds
( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
let x, y be set ; ::_thesis: ( not y in X or Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
A1: ( not [x,y] in EqR implies Class (EqR,x) misses Class (EqR,y) )
proof
assume A2: not [x,y] in EqR ; ::_thesis: Class (EqR,x) misses Class (EqR,y)
assume  Class (EqR,x) meets Class (EqR,y) ; ::_thesis: contradiction
then consider z being set  such that
A3: z in Class (EqR,x) and
A4: z in Class (EqR,y) by XBOOLE_0:3;
 [z,x] in EqR by A3, Th19;
then A5: [x,z] in EqR by Th6;
 [z,y] in EqR by A4, Th19;
hence  contradiction by A2, A5, Th7; ::_thesis: verum
end;
assume A6: y in X ; ::_thesis: ( Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) )
 ( [x,y] in EqR implies Class (EqR,x) = Class (EqR,y) )
proof
assume  [x,y] in EqR ; ::_thesis: Class (EqR,x) = Class (EqR,y)
then  x in Class (EqR,y) by Th19;
hence  Class (EqR,x) = Class (EqR,y) by A6, Th23; ::_thesis: verum
end;
hence  ( Class (EqR,x) = Class (EqR,y) or Class (EqR,x) misses Class (EqR,y) ) by A1; ::_thesis: verum
end;

theorem Th25: :: EQREL_1:25
for X, x being set st x in X holds
Class ((id X),x) = {x}
proof
let X, x be set ; ::_thesis: ( x in X implies Class ((id X),x) = {x} )
A1: now__::_thesis:_for_y_being_set_st_y_in_Class_((id_X),x)_holds_
y_=_x
let y be set ; ::_thesis: ( y in Class ((id X),x) implies y = x )
assume  y in Class ((id X),x) ; ::_thesis: y = x
then  [y,x] in id X by Th19;
hence  y = x by RELAT_1:def_10; ::_thesis: verum
end;
assume  x in X ; ::_thesis: Class ((id X),x) = {x}
then  for y being set holds
( y in Class ((id X),x) iff y = x ) by A1, Th20;
hence  Class ((id X),x) = {x} by TARSKI:def_1; ::_thesis: verum
end;

theorem Th26: :: EQREL_1:26
for X, x being set st x in X holds
Class ((nabla X),x) = X
proof
let X, x be set ; ::_thesis: ( x in X implies Class ((nabla X),x) = X )
assume A1: x in X ; ::_thesis: Class ((nabla X),x) = X
now__::_thesis:_for_y_being_set_st_y_in_X_holds_
y_in_Class_((nabla_X),x)
let y be set ; ::_thesis: ( y in X implies y in Class ((nabla X),x) )
assume  y in X ; ::_thesis: y in Class ((nabla X),x)
then  [y,x] in nabla X by A1, ZFMISC_1:87;
hence  y in Class ((nabla X),x) by Th19; ::_thesis: verum
end;
then  for y being set holds
( y in X iff y in Class ((nabla X),x) ) ;
hence  Class ((nabla X),x) = X by TARSKI:1; ::_thesis: verum
end;

theorem Th27: :: EQREL_1:27
for X being set
for EqR being Equivalence_Relation of X st ex x being set st Class (EqR,x) = X holds
EqR = nabla X
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X st ex x being set st Class (EqR,x) = X holds
EqR = nabla X
let EqR be Equivalence_Relation of X; ::_thesis: ( ex x being set st Class (EqR,x) = X implies EqR = nabla X )
given x being set  such that A1: Class (EqR,x) = X ; ::_thesis: EqR = nabla X
 [:X,X:] c= EqR
proof
let y be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [y,b1] in [:X,X:] or [y,b1] in EqR )
let z be set ; ::_thesis: ( not [y,z] in [:X,X:] or [y,z] in EqR )
assume A2: [y,z] in [:X,X:] ; ::_thesis: [y,z] in EqR
then  z in Class (EqR,x) by A1, ZFMISC_1:87;
then  [z,x] in EqR by Th19;
then A3: [x,z] in EqR by Th6;
 y in Class (EqR,x) by A1, A2, ZFMISC_1:87;
then  [y,x] in EqR by Th19;
hence  [y,z] in EqR by A3, Th7; ::_thesis: verum
end;
hence  EqR = nabla X by XBOOLE_0:def_10; ::_thesis: verum
end;

theorem :: EQREL_1:28
for x, X, y being set
for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
proof
let x, X, y be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: ( x in X implies ( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) ) )
assume A1: x in X ; ::_thesis: ( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
thus  ( [x,y] in EqR1 "\/" EqR2 implies ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) ) ::_thesis: ( ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) implies [x,y] in EqR1 "\/" EqR2 )
proof
defpred S1[ set , set ] means  ex f being FinSequence st
( 1 <= len f & $1 = f . 1 & $2 = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) );
consider Y being Relation of X,X such that
A2: for x, y being set holds
( [x,y] in Y iff ( x in X & y in X & S1[x,y] ) ) from RELSET_1:sch_1();
A3: Y is_transitive_in X
proof
let x be set ; :: according to RELAT_2:def_8 ::_thesis: for b1, b2 being set holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in Y or not [b1,b2] in Y or [x,b2] in Y )
let y, z be set ; ::_thesis: ( not x in X or not y in X or not z in X or not [x,y] in Y or not [y,z] in Y or [x,z] in Y )
assume that
A4: x in X and
A5: y in X and
A6: z in X and
A7: [x,y] in Y and
A8: [y,z] in Y ; ::_thesis: [x,z] in Y
consider g being FinSequence such that
A9: 1 <= len g and
A10: y = g . 1 and
A11: z = g . (len g) and
A12: for i being Element of NAT st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in EqR1 \/ EqR2 by A2, A8;
consider f being FinSequence such that
A13: 1 <= len f and
A14: x = f . 1 and
A15: y = f . (len f) and
A16: for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A2, A7;
set h = f ^ g;
A17: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A18: (len f) + 1 <= (len f) + (len g) by A9, XREAL_1:7;
then A19: (f ^ g) . (len (f ^ g)) = g . (((len g) + (len f)) - (len f)) by A17, FINSEQ_1:23
.= g . (len g) ;
A20: for i being Element of NAT st 1 <= i & i < len (f ^ g) holds
[((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len (f ^ g) implies [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 )
assume that
A21: 1 <= i and
A22: i < len (f ^ g) ; ::_thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
A23: ( ( 1 <= i & i < len f ) or i = len f or len f < i ) by A21, XXREAL_0:1;
now__::_thesis:_[((f_^_g)_._i),((f_^_g)_._(i_+_1))]_in_EqR1_\/_EqR2
percases ( ( 1 <= i & i < len f ) or i = len f or ( (len f) + 1 <= i & i < len (f ^ g) ) ) by A22, A23, NAT_1:13;
supposeA24: ( 1 <= i & i < len f ) ; ::_thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
then  ( 1 <= i + 1 & i + 1 <= len f ) by NAT_1:13;
then  i + 1 in Seg (len f) by FINSEQ_1:1;
then  i + 1 in dom f by FINSEQ_1:def_3;
then A25: (f ^ g) . (i + 1) = f . (i + 1) by FINSEQ_1:def_7;
 i in Seg (len f) by A24, FINSEQ_1:1;
then  i in dom f by FINSEQ_1:def_3;
then  (f ^ g) . i = f . i by FINSEQ_1:def_7;
hence  [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A16, A24, A25; ::_thesis: verum
end;
supposeA26: i = len f ; ::_thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
 len f in Seg (len f) by A13, FINSEQ_1:1;
then  len f in dom f by FINSEQ_1:def_3;
then A27: (f ^ g) . i = y by A15, A26, FINSEQ_1:def_7;
A28: [y,y] in EqR1 by A5, Th5;
(f ^ g) . (i + 1) = g . ((1 + (len f)) - (len f)) by A18, A26, FINSEQ_1:23
.= y by A10 ;
hence  [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A27, A28, XBOOLE_0:def_3; ::_thesis: verum
end;
supposeA29: ( (len f) + 1 <= i & i < len (f ^ g) ) ; ::_thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
then  len f < i by NAT_1:13;
then reconsider k = i - (len f) as Element of NAT by NAT_1:21;
 i < (len f) + (len g) by A29, FINSEQ_1:22;
then A30: i - (len f) < len g by XREAL_1:19;
 ( (len f) + 1 <= i + 1 & i + 1 <= (len f) + (len g) ) by A17, A29, NAT_1:13;
then A31: (f ^ g) . (i + 1) = g . ((1 + i) - (len f)) by FINSEQ_1:23
.= g . ((i - (len f)) + 1) ;
 (1 + (len f)) - (len f) <= i - (len f) by A29, XREAL_1:9;
then  [(g . k),(g . (k + 1))] in EqR1 \/ EqR2 by A12, A30;
hence  [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A17, A29, A31, FINSEQ_1:23; ::_thesis: verum
end;
end;
end;
hence  [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 ; ::_thesis: verum
end;
 1 in Seg (len f) by A13, FINSEQ_1:1;
then  1 in dom f by FINSEQ_1:def_3;
then A32: x = (f ^ g) . 1 by A14, FINSEQ_1:def_7;
 1 <= len (f ^ g) by A13, A17, NAT_1:12;
hence  [x,z] in Y by A2, A4, A6, A11, A32, A19, A20; ::_thesis: verum
end;
A33: Y is_symmetric_in X
proof
let x be set ; :: according to RELAT_2:def_3 ::_thesis: for b1 being set holds
( not x in X or not b1 in X or not [x,b1] in Y or [b1,x] in Y )
let y be set ; ::_thesis: ( not x in X or not y in X or not [x,y] in Y or [y,x] in Y )
assume that
A34: ( x in X & y in X ) and
A35: [x,y] in Y ; ::_thesis: [y,x] in Y
consider f being FinSequence such that
A36: 1 <= len f and
A37: x = f . 1 and
A38: y = f . (len f) and
A39: for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A2, A35;
defpred S2[ Nat, set ] means $2 = f . ((1 + (len f)) - $1);
A40: for k being Nat st k in Seg (len f) holds
ex z being set st S2[k,z] ;
consider g being FinSequence such that
A41: ( dom g = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S2[k,g . k] ) ) from FINSEQ_1:sch_1(A40);
A42: len f = len g by A41, FINSEQ_1:def_3;
A43: for j being Element of NAT st 1 <= j & j < len g holds
[(g . j),(g . (j + 1))] in EqR1 \/ EqR2
proof
let j be Element of NAT ; ::_thesis: ( 1 <= j & j < len g implies [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 )
assume that
A44: 1 <= j and
A45: j < len g ; ::_thesis: [(g . j),(g . (j + 1))] in EqR1 \/ EqR2
reconsider k = (len f) - j as Element of NAT by A42, A45, NAT_1:21;
 j - (len f) < (len f) - (len f) by A42, A45, XREAL_1:9;
then  - ((len f) - j) < - 0 ;
then  0 < k ;
then A46: 0 + 1 <= k by NAT_1:13;
 - j < - 0 by A44, XREAL_1:24;
then  (len f) + (- j) < 0 + (len f) by XREAL_1:6;
then A47: [(f . k),(f . (k + 1))] in EqR1 \/ EqR2 by A39, A46;
A48: now__::_thesis:_[(f_._(k_+_1)),(f_._k)]_in_EqR1_\/_EqR2
percases ( [(f . k),(f . (k + 1))] in EqR1 or [(f . k),(f . (k + 1))] in EqR2 ) by A47, XBOOLE_0:def_3;
suppose [(f . k),(f . (k + 1))] in EqR1 ; ::_thesis: [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2
then  [(f . (k + 1)),(f . k)] in EqR1 by Th6;
hence  [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2 by XBOOLE_0:def_3; ::_thesis: verum
end;
suppose [(f . k),(f . (k + 1))] in EqR2 ; ::_thesis: [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2
then  [(f . (k + 1)),(f . k)] in EqR2 by Th6;
hence  [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2 by XBOOLE_0:def_3; ::_thesis: verum
end;
end;
end;
 ( 1 <= j + 1 & j + 1 <= len f ) by A42, A45, NAT_1:12, NAT_1:13;
then  j + 1 in Seg (len f) by FINSEQ_1:1;
then A49: g . (j + 1) = f . (((len f) + 1) - (1 + j)) by A41
.= f . ((len f) - j) ;
 j in Seg (len f) by A42, A44, A45, FINSEQ_1:1;
then g . j = f . ((1 + (len f)) - j) by A41
.= f . (((len f) - j) + 1) ;
hence  [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 by A49, A48; ::_thesis: verum
end;
 len f in Seg (len f) by A36, FINSEQ_1:1;
then g . (len f) = f . ((1 + (len f)) - (len f)) by A41
.= f . (1 + 0) ;
then A50: x = g . (len g) by A37, A41, FINSEQ_1:def_3;
 1 in Seg (len f) by A36, FINSEQ_1:1;
then A51: g . 1 = f . (((len f) + 1) - 1) by A41
.= f . (len f) ;
 1 <= len g by A36, A41, FINSEQ_1:def_3;
hence  [y,x] in Y by A2, A34, A38, A51, A50, A43; ::_thesis: verum
end;
 Y is_reflexive_in X
proof
let x be set ; :: according to RELAT_2:def_1 ::_thesis: ( not x in X or [x,x] in Y )
assume A52: x in X ; ::_thesis: [x,x] in Y
set g = <*x*>;
A53: for i being Element of NAT st 1 <= i & i < len <*x*> holds
[(<*x*> . i),(<*x*> . (i + 1))] in EqR1 \/ EqR2 by FINSEQ_1:40;
 ( len <*x*> = 1 & <*x*> . 1 = x ) by FINSEQ_1:40;
hence  [x,x] in Y by A2, A52, A53; ::_thesis: verum
end;
then  ( field Y = X & dom Y = X ) by ORDERS_1:13;
then reconsider R1 = Y as Equivalence_Relation of X by A33, A3, PARTFUN1:def_2, RELAT_2:def_11, RELAT_2:def_16;
 for x, y being set st [x,y] in EqR1 \/ EqR2 holds
[x,y] in R1
proof
let x, y be set ; ::_thesis: ( [x,y] in EqR1 \/ EqR2 implies [x,y] in R1 )
assume A54: [x,y] in EqR1 \/ EqR2 ; ::_thesis: [x,y] in R1
set g = <*x,y*>;
A55: len <*x,y*> = 1 + 1 by FINSEQ_1:44;
A56: <*x,y*> . 1 = x by FINSEQ_1:44;
A57: for i being Element of NAT st 1 <= i & i < len <*x,y*> holds
[(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2
proof
let i be Element of NAT ; ::_thesis: ( 1 <= i & i < len <*x,y*> implies [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2 )
assume that
A58: 1 <= i and
A59: i < len <*x,y*> ; ::_thesis: [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2
 i <= 1 by A55, A59, NAT_1:13;
then  1 = i by A58, XXREAL_0:1;
hence  [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2 by A54, A56, FINSEQ_1:44; ::_thesis: verum
end;
 len <*x,y*> = 2 by FINSEQ_1:44;
then A60: ( <*x,y*> . 1 = x & <*x,y*> . (len <*x,y*>) = y ) by FINSEQ_1:44;
 ( x in X & y in X ) by A54, Lm1;
hence  [x,y] in R1 by A2, A55, A60, A57; ::_thesis: verum
end;
then  EqR1 \/ EqR2 c= R1 by RELAT_1:def_3;
then A61: EqR1 "\/" EqR2 c= R1 by Def2;
assume  [x,y] in EqR1 "\/" EqR2 ; ::_thesis: ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) )
then consider f being FinSequence such that
A62: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A2, A61;
take  f ; ::_thesis: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) )
thus  ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A62; ::_thesis: verum
end;
given f being FinSequence such that A63: 1 <= len f and
A64: x = f . 1 and
A65: y = f . (len f) and
A66: for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ; ::_thesis: [x,y] in EqR1 "\/" EqR2
defpred S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in EqR1 "\/" EqR2 );
A67: now__::_thesis:_for_i_being_Element_of_NAT_st_S1[i]_holds_
S1[i_+_1]
let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] )
assume A68: S1[i] ; ::_thesis: S1[i + 1]
thus  S1[i + 1] ::_thesis: verum
proof
assume that
A69: 1 <= i + 1 and
A70: i + 1 <= len f ; ::_thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
A71: ( 1 <= i or 1 = i + 1 ) by A69, NAT_1:8;
A72: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
A73: i < len f by A70, NAT_1:13;
now__::_thesis:_[(f_._1),(f_._(i_+_1))]_in_EqR1_"\/"_EqR2
percases ( 1 <= i or 0 = i ) by A71;
supposeA74: 1 <= i ; ::_thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
then  [(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A66, A73;
hence  [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 by A68, A70, A72, A74, Th7, NAT_1:13; ::_thesis: verum
end;
supposeA75: 0 = i ; ::_thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
 [(f . 1),(f . 1)] in EqR1 by A1, A64, Th5;
then  [(f . 1),(f . 1)] in EqR1 \/ EqR2 by XBOOLE_0:def_3;
hence  [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 by A72, A75; ::_thesis: verum
end;
end;
end;
hence  [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 ; ::_thesis: verum
end;
end;
A76: S1[ 0 ] ;
 for i being Element of NAT holds S1[i] from NAT_1:sch_1(A76, A67);
hence  [x,y] in EqR1 "\/" EqR2 by A63, A64, A65; ::_thesis: verum
end;

theorem Th29: :: EQREL_1:29
for X being set
for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
proof
let X be set ; ::_thesis: for EqR1, EqR2, E being Equivalence_Relation of X st E = EqR1 \/ EqR2 holds
for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
let EqR1, EqR2, E be Equivalence_Relation of X; ::_thesis: ( E = EqR1 \/ EqR2 implies for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) )
assume A1: E = EqR1 \/ EqR2 ; ::_thesis: for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
 for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
proof
let x be set ; ::_thesis: ( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
assume  x in X ; ::_thesis: ( Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) )
assume that
A2: not Class (E,x) = Class (EqR1,x) and
A3: not Class (E,x) = Class (EqR2,x) ; ::_thesis: contradiction
consider y being set  such that
A4: ( ( y in Class (E,x) & not y in Class (EqR1,x) ) or ( y in Class (EqR1,x) & not y in Class (E,x) ) ) by A2, TARSKI:1;
A5: now__::_thesis:_(_y_in_Class_(EqR1,x)_implies_y_in_Class_(E,x)_)
assume that
A6: y in Class (EqR1,x) and
A7: not y in Class (E,x) ; ::_thesis: contradiction
 [y,x] in EqR1 by A6, Th19;
then  [y,x] in E by A1, XBOOLE_0:def_3;
hence  contradiction by A7, Th19; ::_thesis: verum
end;
then A8: [y,x] in E by A4, Th19;
consider z being set  such that
A9: ( ( z in Class (E,x) & not z in Class (EqR2,x) ) or ( z in Class (EqR2,x) & not z in Class (E,x) ) ) by A3, TARSKI:1;
A10: now__::_thesis:_(_z_in_Class_(EqR2,x)_implies_z_in_Class_(E,x)_)
assume that
A11: z in Class (EqR2,x) and
A12: not z in Class (E,x) ; ::_thesis: contradiction
 [z,x] in EqR2 by A11, Th19;
then  [z,x] in E by A1, XBOOLE_0:def_3;
hence  contradiction by A12, Th19; ::_thesis: verum
end;
then A13: [z,x] in E by A9, Th19;
 not [z,x] in EqR2 by A9, A10, Th19;
then A14: [z,x] in EqR1 by A1, A13, XBOOLE_0:def_3;
A15: now__::_thesis:_not_[y,z]_in_EqR1
assume  [y,z] in EqR1 ; ::_thesis: contradiction
then A16: [z,y] in EqR1 by Th6;
 [x,z] in EqR1 by A14, Th6;
then  [x,y] in EqR1 by A16, Th7;
then  [y,x] in EqR1 by Th6;
hence  contradiction by A4, A5, Th19; ::_thesis: verum
end;
 not [y,x] in EqR1 by A4, A5, Th19;
then A17: [y,x] in EqR2 by A1, A8, XBOOLE_0:def_3;
A18: now__::_thesis:_not_[y,z]_in_EqR2
assume A19: [y,z] in EqR2 ; ::_thesis: contradiction
 [x,y] in EqR2 by A17, Th6;
then  [x,z] in EqR2 by A19, Th7;
then  [z,x] in EqR2 by Th6;
hence  contradiction by A9, A10, Th19; ::_thesis: verum
end;
 [x,z] in E by A13, Th6;
then  [y,z] in E by A8, Th7;
hence  contradiction by A1, A18, A15, XBOOLE_0:def_3; ::_thesis: verum
end;
hence  for x being set holds
( not x in X or Class (E,x) = Class (EqR1,x) or Class (E,x) = Class (EqR2,x) ) ; ::_thesis: verum
end;

theorem :: EQREL_1:30
for X being set
for EqR1, EqR2 being Equivalence_Relation of X holds
( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
proof
let X be set ; ::_thesis: for EqR1, EqR2 being Equivalence_Relation of X holds
( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
let EqR1, EqR2 be Equivalence_Relation of X; ::_thesis: ( not EqR1 \/ EqR2 = nabla X or EqR1 = nabla X or EqR2 = nabla X )
assume A1: EqR1 \/ EqR2 = nabla X ; ::_thesis: ( EqR1 = nabla X or EqR2 = nabla X )
 ( X = {} or EqR1 = nabla X or EqR2 = nabla X )
proof
set y = the Element of X;
A2: now__::_thesis:_for_x_being_set_holds_
(_not_x_in_X_or_Class_(EqR1,x)_=_X_or_Class_(EqR2,x)_=_X_)
let x be set ; ::_thesis: ( not x in X or Class (EqR1,x) = X or Class (EqR2,x) = X )
assume A3: x in X ; ::_thesis: ( Class (EqR1,x) = X or Class (EqR2,x) = X )
then  ( Class ((nabla X),x) = Class (EqR1,x) or Class ((nabla X),x) = Class (EqR2,x) ) by A1, Th29;
hence  ( Class (EqR1,x) = X or Class (EqR2,x) = X ) by A3, Th26; ::_thesis: verum
end;
assume  X <> {} ; ::_thesis: ( EqR1 = nabla X or EqR2 = nabla X )
then  ( Class (EqR1, the Element of X) = X or Class (EqR2, the Element of X) = X ) by A2;
hence  ( EqR1 = nabla X or EqR2 = nabla X ) by Th27; ::_thesis: verum
end;
hence  ( EqR1 = nabla X or EqR2 = nabla X ) ; ::_thesis: verum
end;

definition
let X be set ;
let EqR be Equivalence_Relation of X;
func Class EqR ->  Subset-Family of X means :Def3: :: EQREL_1:def 3
 for A being Subset of X holds
( A in it iff ex x being set st
( x in X & A = Class (EqR,x) ) );
existence
 ex b1 being Subset-Family of X st
for A being Subset of X holds
( A in b1 iff ex x being set st
( x in X & A = Class (EqR,x) ) )
proof
defpred S1[ set ] means  ex x being set st
( x in X & $1 = Class (EqR,x) );
consider F being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
take  F ; ::_thesis: for A being Subset of X holds
( A in F iff ex x being set st
( x in X & A = Class (EqR,x) ) )
thus  for A being Subset of X holds
( A in F iff ex x being set st
( x in X & A = Class (EqR,x) ) ) by A1; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset-Family of X st ( for A being Subset of X holds
( A in b1 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ) & ( for A being Subset of X holds
( A in b2 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ) holds
b1 = b2
proof
let F1, F2 be Subset-Family of X; ::_thesis: ( ( for A being Subset of X holds
( A in F1 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ) & ( for A being Subset of X holds
( A in F2 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ) implies F1 = F2 )
assume that
A2: for A being Subset of X holds
( A in F1 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) and
A3: for A being Subset of X holds
( A in F2 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) ; ::_thesis: F1 = F2
now__::_thesis:_for_A_being_Subset_of_X_holds_
(_A_in_F1_iff_A_in_F2_)
let A be Subset of X; ::_thesis: ( A in F1 iff A in F2 )
 ( A in F1 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) by A2;
hence  ( A in F1 iff A in F2 ) by A3; ::_thesis: verum
end;
hence  F1 = F2 by SETFAM_1:31; ::_thesis: verum
end;
end;

:: deftheorem Def3 defines Class EQREL_1:def_3_:_
 for X being set
for EqR being Equivalence_Relation of X
for b3 being Subset-Family of X holds
( b3 = Class EqR iff for A being Subset of X holds
( A in b3 iff ex x being set st
( x in X & A = Class (EqR,x) ) ) );

theorem Th31: :: EQREL_1:31
for X being set
for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X st X = {} holds
Class EqR = {}
let EqR be Equivalence_Relation of X; ::_thesis: ( X = {} implies Class EqR = {} )
assume that
A1: X = {} and
A2: Class EqR <> {} ; ::_thesis: contradiction
set z = the Element of Class EqR;
 the Element of Class EqR is Subset of X by A2, TARSKI:def_3;
then  ex x being set st
( x in X & the Element of Class EqR = Class (EqR,x) ) by A2, Def3;
hence  contradiction by A1; ::_thesis: verum
end;

definition
let X be set ;
mode a_partition of X ->  Subset-Family of X means :Def4: :: EQREL_1:def 4
( union it = X & ( for A being Subset of X st A in it holds
( A <> {} & ( for B being Subset of X holds
( not B in it or A = B or A misses B ) ) ) ) );
existence
 ex b1 being Subset-Family of X st
( union b1 = X & ( for A being Subset of X st A in b1 holds
( A <> {} & ( for B being Subset of X holds
( not B in b1 or A = B or A misses B ) ) ) ) )
proof
defpred S1[ set ] means  ex x being set st
( x in X & $1 = {x} );
consider F being Subset-Family of X such that
A1: for A being Subset of X holds
( A in F iff S1[A] ) from SUBSET_1:sch_3();
A2: for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) )
proof
let A be Subset of X; ::_thesis: ( A in F implies ( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) )
assume  A in F ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) )
then consider x being set  such that
 x in X and
A3: A = {x} by A1;
thus  A <> {} by A3; ::_thesis: for B being Subset of X holds
( not B in F or A = B or A misses B )
let B be Subset of X; ::_thesis: ( not B in F or A = B or A misses B )
assume  B in F ; ::_thesis: ( A = B or A misses B )
then consider y being set  such that
 y in X and
A4: B = {y} by A1;
now__::_thesis:_(_not_x_=_y_implies_A_misses_B_)
assume A5: not x = y ; ::_thesis: A misses B
 for z being set st z in A holds
not z in B
proof
let z be set ; ::_thesis: ( z in A implies not z in B )
assume  z in A ; ::_thesis: not z in B
then  not z = y by A3, A5, TARSKI:def_1;
hence  not z in B by A4, TARSKI:def_1; ::_thesis: verum
end;
hence  A misses B by XBOOLE_0:3; ::_thesis: verum
end;
hence  ( A = B or A misses B ) by A3, A4; ::_thesis: verum
end;
take  F ; ::_thesis: ( union F = X & ( for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) ) )
now__::_thesis:_for_y_being_set_holds_
(_y_in_X_iff_ex_Z_being_set_st_
(_y_in_Z_&_Z_in_F_)_)
let y be set ; ::_thesis: ( y in X iff ex Z being set st
( y in Z & Z in F ) )
now__::_thesis:_(_y_in_X_implies_ex_Z_being_set_st_
(_y_in_Z_&_Z_in_F_)_)
set Z = {y};
assume A6: y in X ; ::_thesis: ex Z being set st
( y in Z & Z in F )
then  {y} is Subset of X by ZFMISC_1:31;
then  ( y in {y} & {y} in F ) by A1, A6, TARSKI:def_1;
hence  ex Z being set st
( y in Z & Z in F ) ; ::_thesis: verum
end;
hence  ( y in X iff ex Z being set st
( y in Z & Z in F ) ) ; ::_thesis: verum
end;
hence  ( union F = X & ( for A being Subset of X st A in F holds
( A <> {} & ( for B being Subset of X holds
( not B in F or A = B or A misses B ) ) ) ) ) by A2, TARSKI:def_4; ::_thesis: verum
end;
end;

:: deftheorem Def4 defines a_partition EQREL_1:def_4_:_
 for X being set
for b2 being Subset-Family of X holds
( b2 is a_partition of X iff ( union b2 = X & ( for A being Subset of X st A in b2 holds
( A <> {} & ( for B being Subset of X holds
( not B in b2 or A = B or A misses B ) ) ) ) ) );

theorem Th32: :: EQREL_1:32
for P being a_partition of {} holds P = {}
proof
let P be a_partition of {} ; ::_thesis: P = {}
assume  not P = {} ; ::_thesis: contradiction
then consider Z being set  such that
A1: Z in P by XBOOLE_0:def_1;
 Z <> {} by A1, Def4;
hence  contradiction by A1; ::_thesis: verum
end;

theorem Th33: :: EQREL_1:33
for X being set
for EqR being Equivalence_Relation of X holds Class EqR is a_partition of X
proof
let X be set ; ::_thesis: for EqR being Equivalence_Relation of X holds Class EqR is a_partition of X
let EqR be Equivalence_Relation of X; ::_thesis: Class EqR is a_partition of X
now__::_thesis:_for_x_being_set_holds_
(_x_in_X_iff_ex_Z_being_set_st_
(_x_in_Z_&_Z_in_Class_EqR_)_)
let x be set ; ::_thesis: ( x in X iff ex Z being set st
( x in Z & Z in Class EqR ) )
now__::_thesis:_(_x_in_X_implies_ex_Z_being_set_st_
(_x_in_Z_&_Z_in_Class_EqR_)_)
consider Z being set  such that
A1: Z = Class (EqR,x) ;
assume A2: x in X ; ::_thesis: ex Z being set st
( x in Z & Z in Class EqR )
then  Z in Class EqR by A1, Def3;
hence  ex Z being set st
( x in Z & Z in Class EqR ) by A2, A1, Th20; ::_thesis: verum
end;
hence  ( x in X iff ex Z being set st
( x in Z & Z in Class EqR ) ) ; ::_thesis: verum
end;
hence  union (Class EqR) = X by TARSKI:def_4; :: according to EQREL_1:def_4 ::_thesis: for A being Subset of X st A in Class EqR holds
( A <> {} & ( for B being Subset of X holds
( not B in Class EqR or A = B or A misses B ) ) )
let A be Subset of X; ::_thesis: ( A in Class EqR implies ( A <> {} & ( for B being Subset of X holds
( not B in Class EqR or A = B or A misses B ) ) ) )
assume  A in Class EqR ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in Class EqR or A = B or A misses B ) ) )
then A3: ex x being set st
( x in X & A = Class (EqR,x) ) by Def3;
hence  A <> {} by Th20; ::_thesis: for B being Subset of X holds
( not B in Class EqR or A = B or A misses B )
let B be Subset of X; ::_thesis: ( not B in Class EqR or A = B or A misses B )
assume  B in Class EqR ; ::_thesis: ( A = B or A misses B )
then  ex y being set st
( y in X & B = Class (EqR,y) ) by Def3;
hence  ( A = B or A misses B ) by A3, Th24; ::_thesis: verum
end;

theorem Th34: :: EQREL_1:34
for X being set
for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR
proof
let X be set ; ::_thesis: for P being a_partition of X ex EqR being Equivalence_Relation of X st P = Class EqR
let P be a_partition of X; ::_thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
A1: ( X <> {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )
proof
defpred S1[ set , set ] means  ex A being Subset of X st
( A in P & $1 in A & $2 in A );
assume  X <> {} ; ::_thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
A2: for x, y, z being set st S1[x,y] & S1[y,z] holds
S1[x,z]
proof
let x, y, z be set ; ::_thesis: ( S1[x,y] & S1[y,z] implies S1[x,z] )
given A being Subset of X such that A3: A in P and
A4: ( x in A & y in A ) ; ::_thesis: ( not S1[y,z] or S1[x,z] )
given B being Subset of X such that A5: B in P and
A6: ( y in B & z in B ) ; ::_thesis: S1[x,z]
 ( A = B or A misses B ) by A3, A5, Def4;
hence  S1[x,z] by A3, A4, A6, XBOOLE_0:3; ::_thesis: verum
end;
A7: union P = X by Def4;
A8: for x being set st x in X holds
S1[x,x]
proof
let x be set ; ::_thesis: ( x in X implies S1[x,x] )
assume  x in X ; ::_thesis: S1[x,x]
then consider Z being set  such that
A9: x in Z and
A10: Z in P by A7, TARSKI:def_4;
reconsider A = Z as Subset of X by A10;
take  A ; ::_thesis: ( A in P & x in A & x in A )
thus  ( A in P & x in A & x in A ) by A9, A10; ::_thesis: verum
end;
A11: for x, y being set st S1[x,y] holds
S1[y,x] ;
consider R being Equivalence_Relation of X such that
A12: for x, y being set holds
( [x,y] in R iff ( x in X & y in X & S1[x,y] ) ) from EQREL_1:sch_1(A8, A11, A2);
take  R ; ::_thesis: P = Class R
now__::_thesis:_for_A_being_Subset_of_X_holds_
(_A_in_P_iff_A_in_Class_R_)
let A be Subset of X; ::_thesis: ( A in P iff A in Class R )
A13: now__::_thesis:_(_A_in_P_implies_A_in_Class_R_)
set x = the Element of A;
assume A14: A in P ; ::_thesis: A in Class R
then A15: A <> {} by Def4;
then A16: the Element of A in X by TARSKI:def_3;
now__::_thesis:_for_y_being_set_holds_
(_y_in_A_iff_y_in_Class_(R,_the_Element_of_A)_)
let y be set ; ::_thesis: ( y in A iff y in Class (R, the Element of A) )
A17: now__::_thesis:_(_y_in_Class_(R,_the_Element_of_A)_implies_y_in_A_)
assume  y in Class (R, the Element of A) ; ::_thesis: y in A
then  [y, the Element of A] in R by Th19;
then consider B being Subset of X such that
A18: ( B in P & y in B ) and
A19: the Element of A in B by A12;
 A meets B by A15, A19, XBOOLE_0:3;
hence  y in A by A14, A18, Def4; ::_thesis: verum
end;
now__::_thesis:_(_y_in_A_implies_y_in_Class_(R,_the_Element_of_A)_)
assume  y in A ; ::_thesis: y in Class (R, the Element of A)
then  [y, the Element of A] in R by A12, A14, A16;
hence  y in Class (R, the Element of A) by Th19; ::_thesis: verum
end;
hence  ( y in A iff y in Class (R, the Element of A) ) by A17; ::_thesis: verum
end;
then  A = Class (R, the Element of A) by TARSKI:1;
hence  A in Class R by A16, Def3; ::_thesis: verum
end;
now__::_thesis:_(_A_in_Class_R_implies_A_in_P_)
assume  A in Class R ; ::_thesis: A in P
then consider x being set  such that
A20: x in X and
A21: A = Class (R,x) by Def3;
 x in Class (R,x) by A20, Th20;
then  [x,x] in R by Th19;
then consider B being Subset of X such that
A22: B in P and
A23: x in B and
 x in B by A12;
now__::_thesis:_for_y_being_set_holds_
(_y_in_A_iff_y_in_B_)
let y be set ; ::_thesis: ( y in A iff y in B )
A24: now__::_thesis:_(_y_in_A_implies_y_in_B_)
assume  y in A ; ::_thesis: y in B
then  [y,x] in R by A21, Th19;
then consider C being Subset of X such that
A25: ( C in P & y in C ) and
A26: x in C by A12;
 B meets C by A23, A26, XBOOLE_0:3;
hence  y in B by A22, A25, Def4; ::_thesis: verum
end;
now__::_thesis:_(_y_in_B_implies_y_in_A_)
assume  y in B ; ::_thesis: y in A
then  [y,x] in R by A12, A22, A23;
hence  y in A by A21, Th19; ::_thesis: verum
end;
hence  ( y in A iff y in B ) by A24; ::_thesis: verum
end;
hence  A in P by A22, TARSKI:1; ::_thesis: verum
end;
hence  ( A in P iff A in Class R ) by A13; ::_thesis: verum
end;
hence  P = Class R by SETFAM_1:31; ::_thesis: verum
end;
 ( X = {} implies ex EqR being Equivalence_Relation of X st P = Class EqR )
proof
set EqR1 = the Equivalence_Relation of X;
assume A27: X = {} ; ::_thesis: ex EqR being Equivalence_Relation of X st P = Class EqR
take  the Equivalence_Relation of X ; ::_thesis: P = Class the Equivalence_Relation of X
 P = {} by A27, Th32;
hence  P = Class the Equivalence_Relation of X by A27, Th31; ::_thesis: verum
end;
hence  ex EqR being Equivalence_Relation of X st P = Class EqR by A1; ::_thesis: verum
end;

theorem :: EQREL_1:35
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) ) by Lm2;

theorem :: EQREL_1:36
for x, X being set
for EqR being Equivalence_Relation of X st x in Class EqR holds
ex y being Element of X st x = Class (EqR,y)
proof
let x, X be set ; ::_thesis: for EqR being Equivalence_Relation of X st x in Class EqR holds
ex y being Element of X st x = Class (EqR,y)
let EqR be Equivalence_Relation of X; ::_thesis: ( x in Class EqR implies ex y being Element of X st x = Class (EqR,y) )
assume A1: x in Class EqR ; ::_thesis: ex y being Element of X st x = Class (EqR,y)
then reconsider x = x as Subset of X ;
consider y being set  such that
A2: y in X and
A3: x = Class (EqR,y) by A1, Def3;
reconsider y = y as Element of X by A2;
take  y ; ::_thesis: x = Class (EqR,y)
thus  x = Class (EqR,y) by A3; ::_thesis: verum
end;

begin

registration
let X be non empty set ;
cluster  ->  non empty for a_partition of X;
coherence
 for b1 being a_partition of X holds not b1 is empty
proof
set x = the Element of X;
let P be a_partition of X; ::_thesis: not P is empty
 union P = X by Def4;
then  ex A being set st
( the Element of X in A & A in P ) by TARSKI:def_4;
hence  not P is empty ; ::_thesis: verum
end;
end;

registration
let X be set ;
cluster  ->  with_non-empty_elements for a_partition of X;
coherence
 for b1 being a_partition of X holds b1 is with_non-empty_elements
proof
let P be a_partition of X; ::_thesis: P is with_non-empty_elements
assume  {} in P ; :: according to SETFAM_1:def_8 ::_thesis: contradiction
hence  contradiction by Def4; ::_thesis: verum
end;
end;

definition
let X be set ;
let R be Equivalence_Relation of X;
:: original: Class
redefine func Class R ->  a_partition of X;
coherence
 Class R is a_partition of X by Th33;
end;

registration
let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R ->  non empty ;
coherence
 not Class R is empty ;
end;

registration
let I be non empty set ;
let R be Equivalence_Relation of I;
cluster Class R ->  with_non-empty_elements ;
coherence
 Class R is with_non-empty_elements ;
end;

notation
let I be non empty set ;
let R be Equivalence_Relation of I;
let x be Element of I;
synonym  EqClass (R,x) for  Class (I,R);
end;

definition
let I be non empty set ;
let R be Equivalence_Relation of I;
let x be Element of I;
:: original: Class
redefine func EqClass (R,x) ->  Element of Class R;
coherence
 Class (R,x) is Element of Class R
proof
thus  Class (R,x) is Element of Class R by Def3; ::_thesis: verum
end;
end;

definition
let X be set ;
func SmallestPartition X ->  a_partition of X equals :: EQREL_1:def 5
 Class (id X);
coherence
 Class (id X) is a_partition of X ;
end;

:: deftheorem  defines SmallestPartition EQREL_1:def_5_:_
 for X being set holds SmallestPartition X = Class (id X);

theorem :: EQREL_1:37
for X being non empty set holds SmallestPartition X =  {  {x} where x is Element of X : verum  }
proof
let X be non empty set ; ::_thesis: SmallestPartition X =  {  {x} where x is Element of X : verum  }
set Y =  {  {x} where x is Element of X : verum  }  ;
hereby  :: according to TARSKI:def_3,XBOOLE_0:def_10 ::_thesis:  {  {x} where x is Element of X : verum  }  c= SmallestPartition X
let x be set ; ::_thesis: ( x in SmallestPartition X implies x in  {  {x} where x is Element of X : verum  }  )
assume  x in SmallestPartition X ; ::_thesis: x in  {  {x} where x is Element of X : verum  }
then consider y being set  such that
A1: y in X and
A2: x = Class ((id X),y) by Def3;
 x = {y} by A1, A2, Th25;
hence  x in  {  {x} where x is Element of X : verum  }  by A1; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in  {  {x} where x is Element of X : verum  }  or x in SmallestPartition X )
assume  x in  {  {x} where x is Element of X : verum  }  ; ::_thesis: x in SmallestPartition X
then consider y being Element of X such that
A3: x = {y} ;
 Class ((id X),y) = x by A3, Th25;
hence  x in SmallestPartition X by Def3; ::_thesis: verum
end;


definition
let X be non empty set ;
let x be Element of X;
let S1 be a_partition of X;
func EqClass (x,S1) ->  Subset of X means :Def6: :: EQREL_1:def 6
( x in it & it in S1 );
existence
 ex b1 being Subset of X st
( x in b1 & b1 in S1 )
proof
consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
take  Class (EQR,x) ; ::_thesis: ( x in Class (EQR,x) & Class (EQR,x) in S1 )
thus  x in Class (EQR,x) by Th20; ::_thesis: Class (EQR,x) in S1
thus  Class (EQR,x) in S1 by A1, Def3; ::_thesis: verum
end;
uniqueness
 for b1, b2 being Subset of X st x in b1 & b1 in S1 & x in b2 & b2 in S1 holds
b1 = b2
proof
let A, B be Subset of X; ::_thesis: ( x in A & A in S1 & x in B & B in S1 implies A = B )
assume that
A2: x in A and
A3: A in S1 and
A4: x in B and
A5: B in S1 ; ::_thesis: A = B
 A meets B by A2, A4, XBOOLE_0:3;
hence  A = B by A3, A5, Def4; ::_thesis: verum
end;
end;

:: deftheorem Def6 defines EqClass EQREL_1:def_6_:_
 for X being non empty set
for x being Element of X
for S1 being a_partition of X
for b4 being Subset of X holds
( b4 = EqClass (x,S1) iff ( x in b4 & b4 in S1 ) );

theorem Th38: :: EQREL_1:38
for X being non empty set
for S1, S2 being a_partition of X st ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) holds
S1 = S2
proof
let X be non empty set ; ::_thesis: for S1, S2 being a_partition of X st ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) holds
S1 = S2
let S1, S2 be a_partition of X; ::_thesis: ( ( for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ) implies S1 = S2 )
assume A1: for x being Element of X holds EqClass (x,S1) = EqClass (x,S2) ; ::_thesis: S1 = S2
now__::_thesis:_for_P_being_Subset_of_X_holds_
(_(_P_in_S1_implies_P_in_S2_)_&_(_P_in_S2_implies_P_in_S1_)_)
let P be Subset of X; ::_thesis: ( ( P in S1 implies P in S2 ) & ( P in S2 implies P in S1 ) )
thus  ( P in S1 implies P in S2 ) ::_thesis: ( P in S2 implies P in S1 )
proof
set x = the Element of P;
assume A2: P in S1 ; ::_thesis: P in S2
then A3: not P is empty by Def4;
then  the Element of P in P ;
then reconsider x = the Element of P as Element of X ;
 P = EqClass (x,S1) by A2, A3, Def6;
then  P = EqClass (x,S2) by A1;
hence  P in S2 by Def6; ::_thesis: verum
end;
thus  ( P in S2 implies P in S1 ) ::_thesis: verum
proof
set x = the Element of P;
assume A4: P in S2 ; ::_thesis: P in S1
then A5: P <> {} by Def4;
then  the Element of P in P ;
then reconsider x = the Element of P as Element of X ;
 P = EqClass (x,S2) by A4, A5, Def6;
then  P = EqClass (x,S1) by A1;
hence  P in S1 by Def6; ::_thesis: verum
end;
end;
hence  S1 = S2 by SETFAM_1:31; ::_thesis: verum
end;

theorem Th39: :: EQREL_1:39
for X being non empty set holds {X} is a_partition of X
proof
let X be non empty set ; ::_thesis: {X} is a_partition of X
reconsider A1 = {X} as Subset-Family of X by ZFMISC_1:68;
A1: for A being Subset of X st A in A1 holds
( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) )
proof
let A be Subset of X; ::_thesis: ( A in A1 implies ( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) ) )
assume A2: A in A1 ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in A1 or A = B or A misses B ) ) )
hence  A <> {} by TARSKI:def_1; ::_thesis: for B being Subset of X holds
( not B in A1 or A = B or A misses B )
let B be Subset of X; ::_thesis: ( not B in A1 or A = B or A misses B )
assume  B in A1 ; ::_thesis: ( A = B or A misses B )
then  B = X by TARSKI:def_1;
hence  ( A = B or A misses B ) by A2, TARSKI:def_1; ::_thesis: verum
end;
 union A1 = X by ZFMISC_1:25;
hence  {X} is a_partition of X by A1, Def4; ::_thesis: verum
end;

definition
let X be set ;
mode Family-Class of X is Subset-Family of (bool X);
end;

definition
let X be set ;
let F be Family-Class of X;
attrF is partition-membered  means :Def7: :: EQREL_1:def 7
 for S being set st S in F holds
S is a_partition of X;
end;

:: deftheorem Def7 defines partition-membered EQREL_1:def_7_:_
 for X being set
for F being Family-Class of X holds
( F is partition-membered iff for S being set st S in F holds
S is a_partition of X );

registration
let X be set ;
cluster partition-membered for Element of bool (bool (bool X));
existence
 ex b1 being Family-Class of X st b1 is partition-membered
proof
reconsider E = {} as Family-Class of X by XBOOLE_1:2;
take  E ; ::_thesis: E is partition-membered
let S be set ; :: according to EQREL_1:def_7 ::_thesis: ( S in E implies S is a_partition of X )
assume  S in E ; ::_thesis: S is a_partition of X
hence  S is a_partition of X ; ::_thesis: verum
end;
end;

definition
let X be set ;
mode Part-Family of X is partition-membered Family-Class of X;
end;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements for a_partition of X;
existence
 not for b1 being a_partition of X holds b1 is empty
proof
take  {X} ; ::_thesis: ( {X} is Subset-Family of X & {X} is a_partition of X & not {X} is empty )
thus  ( {X} is Subset-Family of X & {X} is a_partition of X & not {X} is empty ) by Th39; ::_thesis: verum
end;
end;

theorem Th40: :: EQREL_1:40
for X being set
for p being a_partition of X holds {p} is Part-Family of X
proof
let X be set ; ::_thesis: for p being a_partition of X holds {p} is Part-Family of X
let p be a_partition of X; ::_thesis: {p} is Part-Family of X
 for x being set st x in {p} holds
x is a_partition of X by TARSKI:def_1;
hence  {p} is Part-Family of X by Def7; ::_thesis: verum
end;

registration
let X be set ;
cluster non empty partition-membered for Element of bool (bool (bool X));
existence
 not for b1 being Part-Family of X holds b1 is empty
proof
set p = the a_partition of X;
reconsider P = { the a_partition of X} as Part-Family of X by Th40;
take  P ; ::_thesis: not P is empty
thus  not P is empty ; ::_thesis: verum
end;
end;

theorem Th41: :: EQREL_1:41
for X being non empty set
for S1 being a_partition of X
for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
proof
let X be non empty set ; ::_thesis: for S1 being a_partition of X
for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
let S1 be a_partition of X; ::_thesis: for x, y being Element of X st EqClass (x,S1) meets EqClass (y,S1) holds
EqClass (x,S1) = EqClass (y,S1)
let x, y be Element of X; ::_thesis: ( EqClass (x,S1) meets EqClass (y,S1) implies EqClass (x,S1) = EqClass (y,S1) )
consider EQR being Equivalence_Relation of X such that
A1: S1 = Class EQR by Th34;
A2: y in Class (EQR,y) by Th20;
 Class (EQR,y) in S1 by A1, Def3;
then A3: Class (EQR,y) = EqClass (y,S1) by A2, Def6;
A4: x in Class (EQR,x) by Th20;
 Class (EQR,x) in S1 by A1, Def3;
then A5: Class (EQR,x) = EqClass (x,S1) by A4, Def6;
assume  EqClass (x,S1) meets EqClass (y,S1) ; ::_thesis: EqClass (x,S1) = EqClass (y,S1)
hence  EqClass (x,S1) = EqClass (y,S1) by A5, A3, Th24; ::_thesis: verum
end;

Lm3:  for X being non empty set
for x being Element of X
for F being Part-Family of X
for A being set st A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
proof
let X be non empty set ; ::_thesis: for x being Element of X
for F being Part-Family of X
for A being set st A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let x be Element of X; ::_thesis: for F being Part-Family of X
for A being set st A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let F be Part-Family of X; ::_thesis: for A being set st A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  holds
ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
let A be set ; ::_thesis: ( A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  implies ex T being a_partition of X st
( T in F & A = EqClass (x,T) ) )
assume  A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ; ::_thesis: ex T being a_partition of X st
( T in F & A = EqClass (x,T) )
then consider S being a_partition of X such that
A1: ( A = EqClass (x,S) & S in F ) ;
take  S ; ::_thesis: ( S in F & A = EqClass (x,S) )
thus  ( S in F & A = EqClass (x,S) ) by A1; ::_thesis: verum
end;

theorem :: EQREL_1:42
for A being set
for X being non empty set
for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
proof
let A be set ; ::_thesis: for X being non empty set
for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
let X be non empty set ; ::_thesis: for S being a_partition of X st A in S holds
ex x being Element of X st A = EqClass (x,S)
let S be a_partition of X; ::_thesis: ( A in S implies ex x being Element of X st A = EqClass (x,S) )
assume A1: A in S ; ::_thesis: ex x being Element of X st A = EqClass (x,S)
then  not A is empty by Def4;
then consider x being set  such that
A2: x in A by XBOOLE_0:def_1;
take  x ; ::_thesis: ( x is Element of X & A = EqClass (x,S) )
thus  ( x is Element of X & A = EqClass (x,S) ) by A1, A2, Def6; ::_thesis: verum
end;

definition
let X be non empty set ;
let F be non empty Part-Family of X;
func Intersection F ->  non empty a_partition of X means :: EQREL_1:def 8
 for x being Element of X holds EqClass (x,it) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ;
uniqueness
 for b1, b2 being non empty a_partition of X st ( for x being Element of X holds EqClass (x,b1) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) & ( for x being Element of X holds EqClass (x,b2) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) holds
b1 = b2
proof
given S1, S2 being a_partition of X such that A1: for x being Element of X holds EqClass (x,S1) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  and
A2: for x being Element of X holds EqClass (x,S2) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  and
A3: not S1 = S2 ; ::_thesis: contradiction
now__::_thesis:_for_x_being_Element_of_X_holds_EqClass_(x,S1)_=_EqClass_(x,S2)
let x be Element of X; ::_thesis: EqClass (x,S1) = EqClass (x,S2)
 EqClass (x,S1) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  by A1;
hence  EqClass (x,S1) = EqClass (x,S2) by A2; ::_thesis: verum
end;
hence  contradiction by A3, Th38; ::_thesis: verum
end;
existence
 ex b1 being non empty a_partition of X st
for x being Element of X holds EqClass (x,b1) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }
proof
thus  ex G being non empty a_partition of X st
for x being Element of X holds EqClass (x,G) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ::_thesis: verum
proof
set G =  {  (meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) where x is Element of X : verum  }  ;
  {  (meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) where x is Element of X : verum  }  c= bool X
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in  {  (meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) where x is Element of X : verum  }  or y in bool X )
assume  y in  {  (meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) where x is Element of X : verum  }  ; ::_thesis: y in bool X
then consider x being Element of X such that
A4: y = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ;
 y c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in y or e in X )
consider T being set  such that
A5: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A5, Def7;
 EqClass (x,T) in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  by A5;
then consider f being set  such that
A6: f in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ;
consider S being a_partition of X such that
A7: f = EqClass (x,S) and
 S in F by A6;
assume  e in y ; ::_thesis: e in X
then  e in EqClass (x,S) by A4, A6, A7, SETFAM_1:def_1;
hence  e in X ; ::_thesis: verum
end;
hence  y in bool X ; ::_thesis: verum
end;
then reconsider G =  {  (meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) where x is Element of X : verum  }  as Subset-Family of X ;
 G is a_partition of X
proof
 X c= union G
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in X or a in union G )
consider T being set  such that
A8: T in F by XBOOLE_0:def_1;
assume  a in X ; ::_thesis: a in union G
then reconsider a1 = a as Element of X ;
reconsider T = T as a_partition of X by A8, Def7;
A9: meet  {  (EqClass (a1,S)) where S is a_partition of X : S in F  }  in G ;
A10: for T being set st T in  {  (EqClass (a1,S)) where S is a_partition of X : S in F  }  holds
a1 in T
proof
let T be set ; ::_thesis: ( T in  {  (EqClass (a1,S)) where S is a_partition of X : S in F  }  implies a1 in T )
assume  T in  {  (EqClass (a1,S)) where S is a_partition of X : S in F  }  ; ::_thesis: a1 in T
then  ex A being a_partition of X st
( T = EqClass (a1,A) & A in F ) ;
hence  a1 in T by Def6; ::_thesis: verum
end;
 EqClass (a1,T) in  {  (EqClass (a1,S)) where S is a_partition of X : S in F  }  by A8;
then  a in meet  {  (EqClass (a1,S)) where S is a_partition of X : S in F  }  by A10, SETFAM_1:def_1;
hence  a in union G by A9, TARSKI:def_4; ::_thesis: verum
end;
hence  union G = X by XBOOLE_0:def_10; :: according to EQREL_1:def_4 ::_thesis: for A being Subset of X st A in G holds
( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) )
let A be Subset of X; ::_thesis: ( A in G implies ( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) ) )
consider T being set  such that
A11: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A11, Def7;
assume A12: A in G ; ::_thesis: ( A <> {} & ( for B being Subset of X holds
( not B in G or A = B or A misses B ) ) )
then consider x being Element of X such that
A13: A = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ;
A14: for Y being set st Y in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  holds
x in Y
proof
let Y be set ; ::_thesis: ( Y in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  implies x in Y )
assume  Y in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ; ::_thesis: x in Y
then  ex T being a_partition of X st
( Y = EqClass (x,T) & T in F ) ;
hence  x in Y by Def6; ::_thesis: verum
end;
 EqClass (x,T) in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  by A11;
hence  A <> {} by A13, A14, SETFAM_1:def_1; ::_thesis: for B being Subset of X holds
( not B in G or A = B or A misses B )
consider x being Element of X such that
A15: A = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  by A12;
let B be Subset of X; ::_thesis: ( not B in G or A = B or A misses B )
assume  B in G ; ::_thesis: ( A = B or A misses B )
then consider y being Element of X such that
A16: B = meet  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  ;
thus  ( A = B or A misses B ) ::_thesis: verum
proof
A17: not  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  is empty
proof
consider T being set  such that
A18: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A18, Def7;
 EqClass (y,T) in  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  by A18;
hence  not  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  is empty ; ::_thesis: verum
end;
A19: not  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  is empty
proof
consider T being set  such that
A20: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A20, Def7;
 EqClass (x,T) in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  by A20;
hence  not  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  is empty ; ::_thesis: verum
end;
now__::_thesis:_(_not_A_meets_B_or_A_=_B_or_A_misses_B_)
assume  A meets B ; ::_thesis: ( A = B or A misses B )
then consider c being set  such that
A21: ( c in A & c in B ) by XBOOLE_0:3;
 c in (meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) /\ (meet  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  ) by A15, A16, A21, XBOOLE_0:def_4;
then A22: c in meet ( {  (EqClass (x,S)) where S is a_partition of X : S in F  }  \/  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  ) by A19, A17, SETFAM_1:9;
A23: now__::_thesis:_for_T_being_a_partition_of_X_st_T_in_F_holds_
c_in_EqClass_(y,T)
let T be a_partition of X; ::_thesis: ( T in F implies c in EqClass (y,T) )
assume  T in F ; ::_thesis: c in EqClass (y,T)
then  EqClass (y,T) in  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  ;
then  EqClass (y,T) in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  \/  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  by XBOOLE_0:def_3;
hence  c in EqClass (y,T) by A22, SETFAM_1:def_1; ::_thesis: verum
end;
A24: now__::_thesis:_for_T_being_a_partition_of_X_st_T_in_F_holds_
c_in_EqClass_(x,T)
let T be a_partition of X; ::_thesis: ( T in F implies c in EqClass (x,T) )
assume  T in F ; ::_thesis: c in EqClass (x,T)
then  EqClass (x,T) in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ;
then  EqClass (x,T) in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  \/  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  by XBOOLE_0:def_3;
hence  c in EqClass (x,T) by A22, SETFAM_1:def_1; ::_thesis: verum
end;
A25: for T being a_partition of X st T in F holds
ex A being set st
( A in EqClass (x,T) & A in EqClass (y,T) )
proof
let T be a_partition of X; ::_thesis: ( T in F implies ex A being set st
( A in EqClass (x,T) & A in EqClass (y,T) ) )
assume A26: T in F ; ::_thesis: ex A being set st
( A in EqClass (x,T) & A in EqClass (y,T) )
take  c ; ::_thesis: ( c in EqClass (x,T) & c in EqClass (y,T) )
thus  ( c in EqClass (x,T) & c in EqClass (y,T) ) by A24, A23, A26; ::_thesis: verum
end;
A27: for T being a_partition of X st T in F holds
EqClass (x,T) meets EqClass (y,T)
proof
let T be a_partition of X; ::_thesis: ( T in F implies EqClass (x,T) meets EqClass (y,T) )
assume  T in F ; ::_thesis: EqClass (x,T) meets EqClass (y,T)
then  ex A being set st
( A in EqClass (x,T) & A in EqClass (y,T) ) by A25;
hence  EqClass (x,T) meets EqClass (y,T) by XBOOLE_0:3; ::_thesis: verum
end;
A28:  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  c=  {  (EqClass (x,S)) where S is a_partition of X : S in F  }
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  or A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  )
assume  A in  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  ; ::_thesis: A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }
then consider T being a_partition of X such that
A29: T in F and
A30: A = EqClass (y,T) by Lm3;
 A = EqClass (x,T) by A27, A29, A30, Th41;
hence  A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  by A29; ::_thesis: verum
end;
  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  c=  {  (EqClass (y,S)) where S is a_partition of X : S in F  }
proof
let A be set ; :: according to TARSKI:def_3 ::_thesis: ( not A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  or A in  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  )
assume  A in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ; ::_thesis: A in  {  (EqClass (y,S)) where S is a_partition of X : S in F  }
then consider T being a_partition of X such that
A31: T in F and
A32: A = EqClass (x,T) by Lm3;
 A = EqClass (y,T) by A27, A31, A32, Th41;
hence  A in  {  (EqClass (y,S)) where S is a_partition of X : S in F  }  by A31; ::_thesis: verum
end;
hence  ( A = B or A misses B ) by A15, A16, A28, XBOOLE_0:def_10; ::_thesis: verum
end;
hence  ( A = B or A misses B ) ; ::_thesis: verum
end;
end;
then reconsider G = G as non empty a_partition of X ;
take  G ; ::_thesis: for x being Element of X holds EqClass (x,G) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }
 for x being Element of X holds EqClass (x,G) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }
proof
let x be Element of X; ::_thesis: EqClass (x,G) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }
A33: now__::_thesis:_for_Y_being_set_st_Y_in__{__(EqClass_(x,S))_where_S_is_a_partition_of_X_:_S_in_F__}__holds_
x_in_Y
let Y be set ; ::_thesis: ( Y in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  implies x in Y )
assume  Y in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ; ::_thesis: x in Y
then  ex T being a_partition of X st
( Y = EqClass (x,T) & T in F ) ;
hence  x in Y by Def6; ::_thesis: verum
end;
 not  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  is empty
proof
consider T being set  such that
A34: T in F by XBOOLE_0:def_1;
reconsider T = T as a_partition of X by A34, Def7;
 EqClass (x,T) in  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  by A34;
hence  not  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  is empty ; ::_thesis: verum
end;
then  ( meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  in G & x in meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ) by A33, SETFAM_1:def_1;
hence  EqClass (x,G) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  by Def6; ::_thesis: verum
end;
hence  for x being Element of X holds EqClass (x,G) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  ; ::_thesis: verum
end;
end;
end;

:: deftheorem  defines Intersection EQREL_1:def_8_:_
 for X being non empty set
for F being non empty Part-Family of X
for b3 being non empty a_partition of X holds
( b3 = Intersection F iff for x being Element of X holds EqClass (x,b3) = meet  {  (EqClass (x,S)) where S is a_partition of X : S in F  }  );

theorem Th43: :: EQREL_1:43
for X being non empty set
for S being a_partition of X
for A being Subset of S holds (union S) \ (union A) = union (S \ A)
proof
let X be non empty set ; ::_thesis: for S being a_partition of X
for A being Subset of S holds (union S) \ (union A) = union (S \ A)
let S be a_partition of X; ::_thesis: for A being Subset of S holds (union S) \ (union A) = union (S \ A)
let A be Subset of S; ::_thesis: (union S) \ (union A) = union (S \ A)
thus  (union S) \ (union A) c= union (S \ A) :: according to XBOOLE_0:def_10 ::_thesis: union (S \ A) c= (union S) \ (union A)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (union S) \ (union A) or y in union (S \ A) )
assume A1: y in (union S) \ (union A) ; ::_thesis: y in union (S \ A)
then  y in union S by XBOOLE_0:def_5;
then consider z being set  such that
A2: y in z and
A3: z in S by TARSKI:def_4;
 not y in union A by A1, XBOOLE_0:def_5;
then  not z in A by A2, TARSKI:def_4;
then  z in S \ A by A3, XBOOLE_0:def_5;
hence  y in union (S \ A) by A2, TARSKI:def_4; ::_thesis: verum
end;
thus  union (S \ A) c= (union S) \ (union A) ::_thesis: verum
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in union (S \ A) or y in (union S) \ (union A) )
assume  y in union (S \ A) ; ::_thesis: y in (union S) \ (union A)
then consider z being set  such that
A4: y in z and
A5: z in S \ A by TARSKI:def_4;
A6: z in S by A5, XBOOLE_0:def_5;
A7: not z in A by A5, XBOOLE_0:def_5;
A8: now__::_thesis:_for_w_being_set_st_w_in_A_holds_
not_y_in_w
let w be set ; ::_thesis: ( w in A implies not y in w )
assume A9: w in A ; ::_thesis: not y in w
then  w in S ;
then  z misses w by A6, A7, A9, Def4;
hence  not y in w by A4, XBOOLE_0:3; ::_thesis: verum
end;
A10: now__::_thesis:_not_y_in_union_A
assume  y in union A ; ::_thesis: contradiction
then  ex v being set st
( y in v & v in A ) by TARSKI:def_4;
hence  contradiction by A8; ::_thesis: verum
end;
 y in union S by A4, A6, TARSKI:def_4;
hence  y in (union S) \ (union A) by A10, XBOOLE_0:def_5; ::_thesis: verum
end;
end;

theorem :: EQREL_1:44
for X being non empty set
for A being Subset of X
for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A
proof
let X be non empty set ; ::_thesis: for A being Subset of X
for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A
let A be Subset of X; ::_thesis: for S being a_partition of X st A in S holds
union (S \ {A}) = X \ A
let S be a_partition of X; ::_thesis: ( A in S implies union (S \ {A}) = X \ A )
assume A1: A in S ; ::_thesis: union (S \ {A}) = X \ A
 {A} c= S
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {A} or y in S )
assume  y in {A} ; ::_thesis: y in S
hence  y in S by A1, TARSKI:def_1; ::_thesis: verum
end;
then reconsider AA = {A} as Subset of S ;
thus  union (S \ {A}) = (union S) \ (union AA) by Th43
.= X \ (union {A}) by Def4
.= X \ A by ZFMISC_1:25 ; ::_thesis: verum
end;

theorem :: EQREL_1:45
{} is a_partition of {}
proof
reconsider A = {} as Subset-Family of {} by XBOOLE_1:2;
 ( union A = {} & ( for a being Subset of {} st a in A holds
( a <> {} & ( for b being Subset of {} holds
( not b in A or a = b or a misses b ) ) ) ) ) ;
hence  {} is a_partition of {} by Def4; ::_thesis: verum
end;

begin


theorem :: EQREL_1:46
for X, X1 being set
for F being Function st X c= F " X1 holds
F .: X c= X1
proof
let X, X1 be set ; ::_thesis: for F being Function st X c= F " X1 holds
F .: X c= X1
let F be Function; ::_thesis: ( X c= F " X1 implies F .: X c= X1 )
assume  X c= F " X1 ; ::_thesis: F .: X c= X1
then A1: F .: X c= F .: (F " X1) by RELAT_1:123;
 F .: (F " X1) c= X1 by FUNCT_1:75;
hence  F .: X c= X1 by A1, XBOOLE_1:1; ::_thesis: verum
end;

theorem Th47: :: EQREL_1:47
for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e
proof
let e, X, Y be set ; ::_thesis: ( e c= [:X,Y:] implies (.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e )
assume  e c= [:X,Y:] ; ::_thesis: (.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e
then  e c= dom (pr1 (X,Y)) by FUNCT_3:def_4;
hence  (.: (pr1 (X,Y))) . e = (pr1 (X,Y)) .: e by FUNCT_3:def_1; ::_thesis: verum
end;

theorem Th48: :: EQREL_1:48
for e, X, Y being set st e c= [:X,Y:] holds
(.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e
proof
let e, X, Y be set ; ::_thesis: ( e c= [:X,Y:] implies (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e )
assume  e c= [:X,Y:] ; ::_thesis: (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e
then  e c= dom (pr2 (X,Y)) by FUNCT_3:def_5;
hence  (.: (pr2 (X,Y))) . e = (pr2 (X,Y)) .: e by FUNCT_3:def_1; ::_thesis: verum
end;

theorem Th49: :: EQREL_1:49
for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
proof
let X, Y be set ; ::_thesis: for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
let X1 be Subset of X; ::_thesis: for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
let Y1 be Subset of Y; ::_thesis: ( [:X1,Y1:] <> {} implies ( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 ) )
assume A1: [:X1,Y1:] <> {} ; ::_thesis: ( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
then A2: X1 <> {} ;
A3: Y1 <> {} by A1;
A4: X <> {} by A2;
now__::_thesis:_for_x_being_set_holds_
(_(_x_in_(pr1_(X,Y))_.:_[:X1,Y1:]_implies_x_in_X1_)_&_(_x_in_X1_implies_x_in_(pr1_(X,Y))_.:_[:X1,Y1:]_)_)
set y = the Element of Y1;
let x be set ; ::_thesis: ( ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) & ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] ) )
thus  ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) ::_thesis: ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] )
proof
assume  x in (pr1 (X,Y)) .: [:X1,Y1:] ; ::_thesis: x in X1
then consider u being set  such that
A5: u in [:X,Y:] and
A6: ( u in [:X1,Y1:] & x = (pr1 (X,Y)) . u ) by FUNCT_2:64;
A7: u `2 in Y by A5, MCART_1:10;
 ( u `1 in X1 & x = (pr1 (X,Y)) . ((u `1),(u `2)) ) by A6, MCART_1:10, MCART_1:21;
hence  x in X1 by A7, FUNCT_3:def_4; ::_thesis: verum
end;
assume A8: x in X1 ; ::_thesis: x in (pr1 (X,Y)) .: [:X1,Y1:]
 the Element of Y1 in Y by A3, TARSKI:def_3;
then A9: x = (pr1 (X,Y)) . (x, the Element of Y1) by A8, FUNCT_3:def_4;
 [x, the Element of Y1] in [:X1,Y1:] by A3, A8, ZFMISC_1:87;
hence  x in (pr1 (X,Y)) .: [:X1,Y1:] by A4, A9, FUNCT_2:35; ::_thesis: verum
end;
hence  (pr1 (X,Y)) .: [:X1,Y1:] = X1 by TARSKI:1; ::_thesis: (pr2 (X,Y)) .: [:X1,Y1:] = Y1
A10: Y <> {} by A3;
now__::_thesis:_for_y_being_set_holds_
(_(_y_in_(pr2_(X,Y))_.:_[:X1,Y1:]_implies_y_in_Y1_)_&_(_y_in_Y1_implies_y_in_(pr2_(X,Y))_.:_[:X1,Y1:]_)_)
set x = the Element of X1;
let y be set ; ::_thesis: ( ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) & ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] ) )
thus  ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) ::_thesis: ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] )
proof
assume  y in (pr2 (X,Y)) .: [:X1,Y1:] ; ::_thesis: y in Y1
then consider u being set  such that
A11: u in [:X,Y:] and
A12: ( u in [:X1,Y1:] & y = (pr2 (X,Y)) . u ) by FUNCT_2:64;
A13: u `1 in X by A11, MCART_1:10;
 ( u `2 in Y1 & y = (pr2 (X,Y)) . ((u `1),(u `2)) ) by A12, MCART_1:10, MCART_1:21;
hence  y in Y1 by A13, FUNCT_3:def_5; ::_thesis: verum
end;
assume A14: y in Y1 ; ::_thesis: y in (pr2 (X,Y)) .: [:X1,Y1:]
 the Element of X1 in X by A2, TARSKI:def_3;
then A15: y = (pr2 (X,Y)) . ( the Element of X1,y) by A14, FUNCT_3:def_5;
 [ the Element of X1,y] in [:X1,Y1:] by A2, A14, ZFMISC_1:87;
hence  y in (pr2 (X,Y)) .: [:X1,Y1:] by A10, A15, FUNCT_2:35; ::_thesis: verum
end;
hence  (pr2 (X,Y)) .: [:X1,Y1:] = Y1 by TARSKI:1; ::_thesis: verum
end;

theorem Th50: :: EQREL_1:50
for X, Y being set
for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
proof
let X, Y be set ; ::_thesis: for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
let X1 be Subset of X; ::_thesis: for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
let Y1 be Subset of Y; ::_thesis: ( [:X1,Y1:] <> {} implies ( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 ) )
assume A1: [:X1,Y1:] <> {} ; ::_thesis: ( (.: (pr1 (X,Y))) . [:X1,Y1:] = X1 & (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1 )
thus (.: (pr1 (X,Y))) . [:X1,Y1:] = (pr1 (X,Y)) .: [:X1,Y1:] by Th47
.= X1 by A1, Th49 ; ::_thesis: (.: (pr2 (X,Y))) . [:X1,Y1:] = Y1
thus (.: (pr2 (X,Y))) . [:X1,Y1:] = (pr2 (X,Y)) .: [:X1,Y1:] by Th48
.= Y1 by A1, Th49 ; ::_thesis: verum
end;

theorem :: EQREL_1:51
for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
proof
let X, Y be set ; ::_thesis: for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
let A be Subset of [:X,Y:]; ::_thesis: for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
let H be Subset-Family of [:X,Y:]; ::_thesis: ( ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) implies [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A )
assume A1: for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; ::_thesis: [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] c= A
let u be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [u,b1] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] or [u,b1] in A )
let v be set ; ::_thesis: ( not [u,v] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] or [u,v] in A )
assume A2: [u,v] in [:(union ((.: (pr1 (X,Y))) .: H)),(meet ((.: (pr2 (X,Y))) .: H)):] ; ::_thesis: [u,v] in A
then A3: v in meet ((.: (pr2 (X,Y))) .: H) by ZFMISC_1:87;
 u in union ((.: (pr1 (X,Y))) .: H) by A2, ZFMISC_1:87;
then consider x being set  such that
A4: u in x and
A5: x in (.: (pr1 (X,Y))) .: H by TARSKI:def_4;
consider y being set  such that
 y in dom (.: (pr1 (X,Y))) and
A6: y in H and
A7: x = (.: (pr1 (X,Y))) . y by A5, FUNCT_1:def_6;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: y = [:X1,Y1:] by A1, A6;
A9: y <> {} by A4, A7, FUNCT_3:8;
 y in bool [:X,Y:] by A6;
then  y in bool (dom (pr2 (X,Y))) by FUNCT_3:def_5;
then  y in dom (.: (pr2 (X,Y))) by FUNCT_3:def_1;
then  (.: (pr2 (X,Y))) . y in (.: (pr2 (X,Y))) .: H by A6, FUNCT_1:def_6;
then  Y1 in (.: (pr2 (X,Y))) .: H by A8, A9, Th50;
then A10: v in Y1 by A3, SETFAM_1:def_1;
 u in X1 by A4, A7, A8, A9, Th50;
then A11: [u,v] in y by A8, A10, ZFMISC_1:87;
 y c= A by A1, A6;
hence  [u,v] in A by A11; ::_thesis: verum
end;

theorem :: EQREL_1:52
for X, Y being set
for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
proof
let X, Y be set ; ::_thesis: for A being Subset of [:X,Y:]
for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
let A be Subset of [:X,Y:]; ::_thesis: for H being Subset-Family of [:X,Y:] st ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) holds
[:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
let H be Subset-Family of [:X,Y:]; ::_thesis: ( ( for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ) implies [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A )
assume A1: for e being set st e in H holds
( e c= A & ex X1 being Subset of X ex Y1 being Subset of Y st e = [:X1,Y1:] ) ; ::_thesis: [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] c= A
let u be set ; :: according to RELAT_1:def_3 ::_thesis: for b1 being set holds
( not [u,b1] in [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] or [u,b1] in A )
let v be set ; ::_thesis: ( not [u,v] in [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] or [u,v] in A )
assume A2: [u,v] in [:(meet ((.: (pr1 (X,Y))) .: H)),(union ((.: (pr2 (X,Y))) .: H)):] ; ::_thesis: [u,v] in A
then A3: u in meet ((.: (pr1 (X,Y))) .: H) by ZFMISC_1:87;
 v in union ((.: (pr2 (X,Y))) .: H) by A2, ZFMISC_1:87;
then consider x being set  such that
A4: v in x and
A5: x in (.: (pr2 (X,Y))) .: H by TARSKI:def_4;
consider y being set  such that
 y in dom (.: (pr2 (X,Y))) and
A6: y in H and
A7: x = (.: (pr2 (X,Y))) . y by A5, FUNCT_1:def_6;
consider X1 being Subset of X, Y1 being Subset of Y such that
A8: y = [:X1,Y1:] by A1, A6;
A9: y <> {} by A4, A7, FUNCT_3:8;
 y in bool [:X,Y:] by A6;
then  y in bool (dom (pr1 (X,Y))) by FUNCT_3:def_4;
then  y in dom (.: (pr1 (X,Y))) by FUNCT_3:def_1;
then  (.: (pr1 (X,Y))) . y in (.: (pr1 (X,Y))) .: H by A6, FUNCT_1:def_6;
then  X1 in (.: (pr1 (X,Y))) .: H by A8, A9, Th50;
then A10: u in X1 by A3, SETFAM_1:def_1;
 v in Y1 by A4, A7, A8, A9, Th50;
then A11: [u,v] in y by A8, A10, ZFMISC_1:87;
 y c= A by A1, A6;
hence  [u,v] in A by A11; ::_thesis: verum
end;

theorem :: EQREL_1:53
for X being set
for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
proof
let X be set ; ::_thesis: for Y being non empty set
for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let Y be non empty set ; ::_thesis: for f being Function of X,Y
for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let f be Function of X,Y; ::_thesis: for H being Subset-Family of X holds union ((.: f) .: H) = f .: (union H)
let H be Subset-Family of X; ::_thesis: union ((.: f) .: H) = f .: (union H)
 dom f = X by FUNCT_2:def_1;
hence  union ((.: f) .: H) = f .: (union H) by FUNCT_3:14; ::_thesis: verum
end;


theorem :: EQREL_1:54
for X being set
for a being Subset-Family of X holds union (union a) = union  {  (union A) where A is Subset of X : A in a  }
proof
let X be set ; ::_thesis: for a being Subset-Family of X holds union (union a) = union  {  (union A) where A is Subset of X : A in a  }
let a be Subset-Family of X; ::_thesis: union (union a) = union  {  (union A) where A is Subset of X : A in a  }
thus  union (union a) c= union  {  (union A) where A is Subset of X : A in a  }  :: according to XBOOLE_0:def_10 ::_thesis: union  {  (union A) where A is Subset of X : A in a  }  c= union (union a)
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union (union a) or e in union  {  (union A) where A is Subset of X : A in a  }  )
assume  e in union (union a) ; ::_thesis: e in union  {  (union A) where A is Subset of X : A in a  }
then consider B being set  such that
A1: e in B and
A2: B in union a by TARSKI:def_4;
consider C being set  such that
A3: B in C and
A4: C in a by A2, TARSKI:def_4;
A5: union C in  {  (union A) where A is Subset of X : A in a  }  by A4;
 e in union C by A1, A3, TARSKI:def_4;
hence  e in union  {  (union A) where A is Subset of X : A in a  }  by A5, TARSKI:def_4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union  {  (union A) where A is Subset of X : A in a  }  or e in union (union a) )
assume  e in union  {  (union A) where A is Subset of X : A in a  }  ; ::_thesis: e in union (union a)
then consider c being set  such that
A6: e in c and
A7: c in  {  (union A) where A is Subset of X : A in a  }  by TARSKI:def_4;
consider A being Subset of X such that
A8: c = union A and
A9: A in a by A7;
consider b being set  such that
A10: e in b and
A11: b in A by A6, A8, TARSKI:def_4;
 b in union a by A9, A11, TARSKI:def_4;
hence  e in union (union a) by A10, TARSKI:def_4; ::_thesis: verum
end;

theorem Th55: :: EQREL_1:55
for X being set
for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
proof
let X be set ; ::_thesis: for D being Subset-Family of X st union D = X holds
for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
let D be Subset-Family of X; ::_thesis: ( union D = X implies for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `) )
assume A1: union D = X ; ::_thesis: for A being Subset of D
for B being Subset of X st B = union A holds
B ` c= union (A `)
let A be Subset of D; ::_thesis: for B being Subset of X st B = union A holds
B ` c= union (A `)
let B be Subset of X; ::_thesis: ( B = union A implies B ` c= union (A `) )
assume A2: B = union A ; ::_thesis: B ` c= union (A `)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in B ` or e in union (A `) )
assume A3: e in B ` ; ::_thesis: e in union (A `)
then consider u being set  such that
A4: e in u and
A5: u in D by A1, TARSKI:def_4;
 not e in B by A3, XBOOLE_0:def_5;
then  not u in A by A2, A4, TARSKI:def_4;
then  u in A ` by A5, SUBSET_1:29;
hence  e in union (A `) by A4, TARSKI:def_4; ::_thesis: verum
end;

theorem :: EQREL_1:56
for X, Y, Z being non empty set
for F being Function of X,Y
for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Y
for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G
let F be Function of X,Y; ::_thesis: for G being Function of X,Z st ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) holds
ex H being Function of Y,Z st H * F = G
let G be Function of X,Z; ::_thesis: ( ( for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ) implies ex H being Function of Y,Z st H * F = G )
defpred S1[ set , set ] means ( for x being Element of X holds not $1 = F . x or for x being Element of X st $1 = F . x holds
$2 = G . x );
assume A1: for x, x9 being Element of X st F . x = F . x9 holds
G . x = G . x9 ; ::_thesis: ex H being Function of Y,Z st H * F = G
A2: now__::_thesis:_for_e_being_set_st_e_in_Y_holds_
ex_u_being_set_st_
(_u_in_Z_&_S1[e,u]_)
let e be set ; ::_thesis: ( e in Y implies ex u being set st
( u in Z & S1[e,u] ) )
assume  e in Y ; ::_thesis: ex u being set st
( u in Z & S1[e,u] )
now__::_thesis:_(_(_ex_x_being_Element_of_X_st_e_=_F_._x_&_ex_u_being_Element_of_Z_st_
(_u_in_Z_&_(_ex_x_being_Element_of_X_st_e_=_F_._x_implies_ex_x_being_Element_of_X_st_
(_e_=_F_._x_&_u_=_G_._x_)_)_)_)_or_(_(_for_x_being_Element_of_X_holds_not_e_=_F_._x_)_&_ex_u_being_set_st_
(_u_in_Z_&_(_ex_x_being_Element_of_X_st_e_=_F_._x_implies_ex_x_being_Element_of_X_st_
(_e_=_F_._x_&_u_=_G_._x_)_)_)_)_)
percases ( ex x being Element of X st e = F . x or for x being Element of X holds not e = F . x ) ;
case ex x being Element of X st e = F . x ; ::_thesis: ex u being Element of Z st
( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) )
then consider x being Element of X such that
A3: e = F . x ;
take u = G . x; ::_thesis: ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) )
thus  ( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) ) by A3; ::_thesis: verum
end;
caseA4: for x being Element of X holds not e = F . x ; ::_thesis: ex u being set st
( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) )
set u = the Element of Z;
 the Element of Z in Z ;
hence  ex u being set st
( u in Z & ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) ) by A4; ::_thesis: verum
end;
end;
end;
then consider u being set  such that
A5: u in Z and
A6: ( ex x being Element of X st e = F . x implies ex x being Element of X st
( e = F . x & u = G . x ) ) ;
take u = u; ::_thesis: ( u in Z & S1[e,u] )
thus  u in Z by A5; ::_thesis: S1[e,u]
thus  S1[e,u] by A1, A6; ::_thesis: verum
end;
consider H being Function of Y,Z such that
A7: for e being set st e in Y holds
S1[e,H . e] from FUNCT_2:sch_1(A2);
take  H ; ::_thesis: H * F = G
now__::_thesis:_for_x_being_Element_of_X_holds_(H_*_F)_._x_=_G_._x
let x be Element of X; ::_thesis: (H * F) . x = G . x
thus (H * F) . x = H . (F . x) by FUNCT_2:15
.= G . x by A7 ; ::_thesis: verum
end;
hence  H * F = G by FUNCT_2:63; ::_thesis: verum
end;

theorem :: EQREL_1:57
for X, Y, Z being non empty set
for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
proof
let X, Y, Z be non empty set ; ::_thesis: for y being Element of Y
for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let y be Element of Y; ::_thesis: for F being Function of X,Y
for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let F be Function of X,Y; ::_thesis: for G being Function of Y,Z holds F " {y} c= (G * F) " {(G . y)}
let G be Function of Y,Z; ::_thesis: F " {y} c= (G * F) " {(G . y)}
 F " {y} c= (G * F) " (Im (G,y)) by FUNCT_2:44;
hence  F " {y} c= (G * F) " {(G . y)} by SETWISEO:8; ::_thesis: verum
end;

theorem :: EQREL_1:58
for X, Y, Z being non empty set
for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Y
for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let F be Function of X,Y; ::_thesis: for x being Element of X
for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let x be Element of X; ::_thesis: for z being Element of Z holds [:F,(id Z):] . (x,z) = [(F . x),z]
let z be Element of Z; ::_thesis: [:F,(id Z):] . (x,z) = [(F . x),z]
thus [:F,(id Z):] . (x,z) = [(F . x),((id Z) . z)] by FUNCT_3:75
.= [(F . x),z] by FUNCT_1:18 ; ::_thesis: verum
end;

theorem :: EQREL_1:59
for X, Y, Z being non empty set
for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Y
for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let F be Function of X,Y; ::_thesis: for A being Subset of X
for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let A be Subset of X; ::_thesis: for B being Subset of Z holds [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
let B be Subset of Z; ::_thesis: [:F,(id Z):] .: [:A,B:] = [:(F .: A),B:]
thus [:F,(id Z):] .: [:A,B:] = [:(F .: A),((id Z) .: B):] by FUNCT_3:72
.= [:(F .: A),B:] by FUNCT_1:92 ; ::_thesis: verum
end;

theorem :: EQREL_1:60
for X, Y, Z being non empty set
for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
proof
let X, Y, Z be non empty set ; ::_thesis: for F being Function of X,Y
for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let F be Function of X,Y; ::_thesis: for y being Element of Y
for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let y be Element of Y; ::_thesis: for z being Element of Z holds [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
let z be Element of Z; ::_thesis: [:F,(id Z):] " {[y,z]} = [:(F " {y}),{z}:]
thus [:F,(id Z):] " {[y,z]} = [:F,(id Z):] " [:{y},{z}:] by ZFMISC_1:29
.= [:(F " {y}),((id Z) " {z}):] by FUNCT_3:73
.= [:(F " {y}),{z}:] by FUNCT_2:94 ; ::_thesis: verum
end;

theorem :: EQREL_1:61
for X being non empty set
for D being Subset-Family of X
for A being Subset of D holds union A is Subset of X
proof
let X be non empty set ; ::_thesis: for D being Subset-Family of X
for A being Subset of D holds union A is Subset of X
let D be Subset-Family of X; ::_thesis: for A being Subset of D holds union A is Subset of X
let A be Subset of D; ::_thesis: union A is Subset of X
 union A c= X
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union A or e in X )
assume  e in union A ; ::_thesis: e in X
then  ex u being set st
( e in u & u in A ) by TARSKI:def_4;
then  e in union D by TARSKI:def_4;
hence  e in X ; ::_thesis: verum
end;
hence  union A is Subset of X ; ::_thesis: verum
end;

theorem :: EQREL_1:62
for X being set
for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
proof
let X be set ; ::_thesis: for D being a_partition of X
for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
let D be a_partition of X; ::_thesis: for A, B being Subset of D holds union (A /\ B) = (union A) /\ (union B)
let A, B be Subset of D; ::_thesis: union (A /\ B) = (union A) /\ (union B)
thus  union (A /\ B) c= (union A) /\ (union B) by ZFMISC_1:79; :: according to XBOOLE_0:def_10 ::_thesis: (union A) /\ (union B) c= union (A /\ B)
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (union A) /\ (union B) or e in union (A /\ B) )
assume A1: e in (union A) /\ (union B) ; ::_thesis: e in union (A /\ B)
then  e in union A by XBOOLE_0:def_4;
then consider a being set  such that
A2: e in a and
A3: a in A by TARSKI:def_4;
A4: a in D by A3;
 e in union B by A1, XBOOLE_0:def_4;
then consider b being set  such that
A5: e in b and
A6: b in B by TARSKI:def_4;
A7: b in D by A6;
 not a misses b by A2, A5, XBOOLE_0:3;
then  a = b by A4, A7, Def4;
then  a in A /\ B by A3, A6, XBOOLE_0:def_4;
hence  e in union (A /\ B) by A2, TARSKI:def_4; ::_thesis: verum
end;

theorem :: EQREL_1:63
for X being non empty set
for D being a_partition of X
for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A `)
proof
let X be non empty set ; ::_thesis: for D being a_partition of X
for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A `)
let D be a_partition of X; ::_thesis: for A being Subset of D
for B being Subset of X st B = union A holds
B ` = union (A `)
let A be Subset of D; ::_thesis: for B being Subset of X st B = union A holds
B ` = union (A `)
let B be Subset of X; ::_thesis: ( B = union A implies B ` = union (A `) )
assume A1: B = union A ; ::_thesis: B ` = union (A `)
 union D = X by Def4;
hence  B ` c= union (A `) by A1, Th55; :: according to XBOOLE_0:def_10 ::_thesis: union (A `) c= B `
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union (A `) or e in B ` )
assume  e in union (A `) ; ::_thesis: e in B `
then consider u being set  such that
A2: e in u and
A3: u in A ` by TARSKI:def_4;
A4: u in D by A3;
assume  not e in B ` ; ::_thesis: contradiction
then  e in B by A2, A4, SUBSET_1:29;
then consider v being set  such that
A5: e in v and
A6: v in A by A1, TARSKI:def_4;
A7: v in D by A6;
 not u misses v by A2, A5, XBOOLE_0:3;
then  u = v by A4, A7, Def4;
hence  contradiction by A3, A6, XBOOLE_0:def_5; ::_thesis: verum
end;

theorem :: EQREL_1:64
for X being non empty set
for E being Equivalence_Relation of X holds not Class E is empty ;

registration
let X be non empty set ;
cluster non empty with_non-empty_elements for a_partition of X;
existence
 not for b1 being a_partition of X holds b1 is empty
proof
reconsider P = Class (nabla X) as a_partition of X ;
take  P ; ::_thesis: not P is empty
thus  not P is empty ; ::_thesis: verum
end;
end;

definition
let X be non empty set ;
let D be non empty a_partition of X;
func proj D ->  Function of X,D means :Def9: :: EQREL_1:def 9
 for p being Element of X holds p in it . p;
existence
 ex b1 being Function of X,D st
for p being Element of X holds p in b1 . p
proof
defpred S1[ set , set ] means $1 in $2;
A1: now__::_thesis:_for_e_being_set_st_e_in_X_holds_
ex_u_being_set_st_
(_u_in_D_&_S1[e,u]_)
A2: union D = X by Def4;
let e be set ; ::_thesis: ( e in X implies ex u being set st
( u in D & S1[e,u] ) )
assume  e in X ; ::_thesis: ex u being set st
( u in D & S1[e,u] )
then  ex u being set st
( e in u & u in D ) by A2, TARSKI:def_4;
hence  ex u being set st
( u in D & S1[e,u] ) ; ::_thesis: verum
end;
consider F being Function of X,D such that
A3: for e being set st e in X holds
S1[e,F . e] from FUNCT_2:sch_1(A1);
take  F ; ::_thesis: for p being Element of X holds p in F . p
let p be Element of X; ::_thesis: p in F . p
thus  p in F . p by A3; ::_thesis: verum
end;
correctness
uniqueness
for b1, b2 being Function of X,D st ( for p being Element of X holds p in b1 . p ) & ( for p being Element of X holds p in b2 . p ) holds
b1 = b2;
proof
let F, G be Function of X,D; ::_thesis: ( ( for p being Element of X holds p in F . p ) & ( for p being Element of X holds p in G . p ) implies F = G )
assume A4: ( ( for p being Element of X holds p in F . p ) & ( for p being Element of X holds p in G . p ) ) ; ::_thesis: F = G
now__::_thesis:_for_x_being_Element_of_X_holds_F_._x_=_G_._x
let x be Element of X; ::_thesis: F . x = G . x
 ( x in F . x & x in G . x ) by A4;
then A5: not F . x misses G . x by XBOOLE_0:3;
 ( F . x is Subset of X & G . x is Subset of X ) by TARSKI:def_3;
hence  F . x = G . x by A5, Def4; ::_thesis: verum
end;
hence  F = G by FUNCT_2:63; ::_thesis: verum
end;
end;

:: deftheorem Def9 defines proj EQREL_1:def_9_:_
 for X being non empty set
for D being non empty a_partition of X
for b3 being Function of X,D holds
( b3 = proj D iff for p being Element of X holds p in b3 . p );

theorem Th65: :: EQREL_1:65
for X being non empty set
for D being non empty a_partition of X
for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p
let D be non empty a_partition of X; ::_thesis: for p being Element of X
for A being Element of D st p in A holds
A = (proj D) . p
let p be Element of X; ::_thesis: for A being Element of D st p in A holds
A = (proj D) . p
let A be Element of D; ::_thesis: ( p in A implies A = (proj D) . p )
assume A1: p in A ; ::_thesis: A = (proj D) . p
 p in (proj D) . p by Def9;
then  ( (proj D) . p is Subset of X & not (proj D) . p misses A ) by A1, TARSKI:def_3, XBOOLE_0:3;
hence  A = (proj D) . p by Def4; ::_thesis: verum
end;

theorem :: EQREL_1:66
for X being non empty set
for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for p being Element of D holds p = (proj D) " {p}
let D be non empty a_partition of X; ::_thesis: for p being Element of D holds p = (proj D) " {p}
let p be Element of D; ::_thesis: p = (proj D) " {p}
thus  p c= (proj D) " {p} :: according to XBOOLE_0:def_10 ::_thesis: (proj D) " {p} c= p
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in p or e in (proj D) " {p} )
assume A1: e in p ; ::_thesis: e in (proj D) " {p}
then  (proj D) . e = p by Th65;
then  (proj D) . e in {p} by TARSKI:def_1;
hence  e in (proj D) " {p} by A1, FUNCT_2:38; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (proj D) " {p} or e in p )
assume A2: e in (proj D) " {p} ; ::_thesis: e in p
then  (proj D) . e in {p} by FUNCT_1:def_7;
then  (proj D) . e = p by TARSKI:def_1;
hence  e in p by A2, Def9; ::_thesis: verum
end;

theorem :: EQREL_1:67
for X being non empty set
for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for A being Subset of D holds (proj D) " A = union A
let D be non empty a_partition of X; ::_thesis: for A being Subset of D holds (proj D) " A = union A
let A be Subset of D; ::_thesis: (proj D) " A = union A
thus  (proj D) " A c= union A :: according to XBOOLE_0:def_10 ::_thesis: union A c= (proj D) " A
proof
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (proj D) " A or e in union A )
assume  e in (proj D) " A ; ::_thesis: e in union A
then  ( (proj D) . e in A & e in (proj D) . e ) by Def9, FUNCT_2:38;
hence  e in union A by TARSKI:def_4; ::_thesis: verum
end;
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in union A or e in (proj D) " A )
assume  e in union A ; ::_thesis: e in (proj D) " A
then consider u being set  such that
A1: e in u and
A2: u in A by TARSKI:def_4;
A3: u in D by A2;
then  (proj D) . e = u by A1, Th65;
hence  e in (proj D) " A by A1, A2, A3, FUNCT_2:38; ::_thesis: verum
end;

theorem :: EQREL_1:68
for X being non empty set
for D being non empty a_partition of X
for W being Element of D ex W9 being Element of X st (proj D) . W9 = W
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for W being Element of D ex W9 being Element of X st (proj D) . W9 = W
let D be non empty a_partition of X; ::_thesis: for W being Element of D ex W9 being Element of X st (proj D) . W9 = W
let W be Element of D; ::_thesis: ex W9 being Element of X st (proj D) . W9 = W
reconsider p = W as Subset of X ;
 p <> {} by Def4;
then consider W9 being Element of X such that
A1: W9 in p by SUBSET_1:4;
take  W9 ; ::_thesis: (proj D) . W9 = W
thus  (proj D) . W9 = W by A1, Th65; ::_thesis: verum
end;

theorem :: EQREL_1:69
for X being non empty set
for D being non empty a_partition of X
for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)
proof
let X be non empty set ; ::_thesis: for D being non empty a_partition of X
for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)
let D be non empty a_partition of X; ::_thesis: for W being Subset of X st ( for B being Subset of X st B in D & B meets W holds
B c= W ) holds
W = (proj D) " ((proj D) .: W)
let W be Subset of X; ::_thesis: ( ( for B being Subset of X st B in D & B meets W holds
B c= W ) implies W = (proj D) " ((proj D) .: W) )
assume A1: for B being Subset of X st B in D & B meets W holds
B c= W ; ::_thesis: W = (proj D) " ((proj D) .: W)
 W c= X ;
then  W c= dom (proj D) by FUNCT_2:def_1;
hence  W c= (proj D) " ((proj D) .: W) by FUNCT_1:76; :: according to XBOOLE_0:def_10 ::_thesis: (proj D) " ((proj D) .: W) c= W
let e be set ; :: according to TARSKI:def_3 ::_thesis: ( not e in (proj D) " ((proj D) .: W) or e in W )
assume A2: e in (proj D) " ((proj D) .: W) ; ::_thesis: e in W
then reconsider d = e as Element of X ;
 (proj D) . e in (proj D) .: W by A2, FUNCT_1:def_7;
then consider c being Element of X such that
A3: c in W and
A4: (proj D) . d = (proj D) . c by FUNCT_2:65;
reconsider B = (proj D) . c as Subset of X by TARSKI:def_3;
 c in (proj D) . c by Def9;
then  B meets W by A3, XBOOLE_0:3;
then A5: B c= W by A1;
 d in B by A4, Def9;
hence  e in W by A5; ::_thesis: verum
end;

theorem :: EQREL_1:70
for X being set
for P being a_partition of X
for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
proof
let X be set ; ::_thesis: for P being a_partition of X
for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
let P be a_partition of X; ::_thesis: for x, a, b being set st x in a & a in P & x in b & b in P holds
a = b
let x, a, b be set ; ::_thesis: ( x in a & a in P & x in b & b in P implies a = b )
assume that
A1: x in a and
A2: a in P and
A3: x in b and
A4: b in P ; ::_thesis: a = b
 a meets b by A1, A3, XBOOLE_0:3;
hence  a = b by A2, A4, Def4; ::_thesis: verum
end;