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 )
assume A5: e in y ; :: thesis: e in X
consider T being set such that
A6: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A6, Def10;
EqClass x,T in { (EqClass x,S) where S is a_partition of X : S in F } by A6;
then consider f being set such that
A7: f in { (EqClass x,S) where S is a_partition of X : S in F } ;
consider S being a_partition of X such that
A8: ( f = EqClass x,S & S in F ) by A7;
e in EqClass x,S by A4, A5, A7, A8, 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

thus union G = X :: according to EQREL_1:def 6 :: 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 ) ) )

proof

thus union G c= X ; :: according to XBOOLE_0:def 10 :: thesis: X c= union G
thus X c= union G :: thesis: verum

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in union G )
assume a in X ; :: thesis: a in union G
then reconsider a1 = a as Element of X ;
consider T being set such that
A9: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A9, Def10;
A10: EqClass a1,T in { (EqClass a1,S) where S is a_partition of X : S in F } by A9;
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 consider A being a_partition of X such that
A11: T = EqClass a1,A and
A in F ;
thus a1 in T by A11, Def8; :: thesis: verum

end;

then A12: a in meet { (EqClass a1,S) where S is a_partition of X : S in F } by A10, SETFAM_1:def 1;
meet { (EqClass a1,S) where S is a_partition of X : S in F } in G ;
hence a in union G by A12, TARSKI:def 4; :: thesis: verum

end;

end;

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 ) ) ) )
assume A13: 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
A14: A = meet { (EqClass x,S) where S is a_partition of X : S in F } ;
consider T being set such that
A15: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A15, Def10;
A16: EqClass x,T in { (EqClass x,S) where S is a_partition of X : S in F } by A15;
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 Def8; :: thesis: verum

end;

hence A <> {} by A14, A16, 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
A17: A = meet { (EqClass x,S) where S is a_partition of X : S in F } by A13;
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
A18: 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

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, Def10;
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;

A21: not { (EqClass y,S) where S is a_partition of X : S in F } is empty

proof

consider T being set such that
A22: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A22, Def10;
EqClass y,T in { (EqClass y,S) where S is a_partition of X : S in F } by A22;
hence not { (EqClass y,S) where S is a_partition of X : S in F } is empty ; :: thesis: verum

end;

now

assume A meets B ; :: thesis: ( A = B or A misses B )
then consider c being set such that
A23: ( 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 A17, A18, A23, XBOOLE_0:def 4;
then A24: 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, A21, SETFAM_1:10;

A25: now

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 A24, SETFAM_1:def 1; :: thesis: verum

end;

A26: now

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 A24, SETFAM_1:def 1; :: thesis: verum

end;

A27: 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 A28: 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 A25, A26, A28; :: thesis: verum

end;

A29: 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 consider A being set such that
A30: ( A in EqClass x,T & A in EqClass y,T ) by A27;
thus EqClass x,T meets EqClass y,T by A30, XBOOLE_0:3; :: thesis: verum

end;

{ (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 }

proof

thus { (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 } :: according to XBOOLE_0:def 10 :: thesis: { (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 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 & A = EqClass x,T ) by Lm4;
A = EqClass y,T by A29, A31, Th50;
hence A in { (EqClass y,S) where S is a_partition of X : S in F } by A31; :: thesis: verum

end;

thus { (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 } :: thesis: verum

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
A32: ( T in F & A = EqClass y,T ) by Lm4;
A = EqClass x,T by A29, A32, Th50;
hence A in { (EqClass x,S) where S is a_partition of X : S in F } by A32; :: thesis: verum

end;

end;

hence ( A = B or A misses B ) by A17, A18; :: 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: 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 }

proof

A34: not { (EqClass x,S) where S is a_partition of X : S in F } is empty

proof

consider T being set such that
A35: T in F by XBOOLE_0:def 1;
reconsider T = T as a_partition of X by A35, Def10;
EqClass x,T in { (EqClass x,S) where S is a_partition of X : S in F } by A35;
hence not { (EqClass x,S) where S is a_partition of X : S in F } is empty ; :: thesis: verum

end;

now

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 Def8; :: thesis: verum

end;

hence x in meet { (EqClass x,S) where S is a_partition of X : S in F } by A34, SETFAM_1:def 1; :: thesis: verum

end;

hence EqClass x,G = meet { (EqClass x,S) where S is a_partition of X : S in F } by A33, Def8; :: 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;