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, Def10;
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, Def10;
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 Def8; :: 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 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 ) ) )
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, Def10;
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 Def8; :: 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, Def10;
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, 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;

now

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:10;

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

end;

A24: 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 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, Th50;
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, Th50;
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

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;

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