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

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

G is 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 }

end;{ (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

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 ;
let y be object ; :: 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 )

reconsider yy = y as set by TARSKI:1;

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 } ;

yy c= X

end;reconsider yy = y as set by TARSKI:1;

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 } ;

yy c= X

proof

hence
y in bool X
; :: thesis: verum
let e be object ; :: according to TARSKI:def 3 :: thesis: ( not e in yy or e in X )

consider T being object 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 yy ; :: 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;consider T being object 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 yy ; :: thesis: e in X

then e in EqClass (x,S) by A4, A6, A7, SETFAM_1:def 1;

hence e in X ; :: thesis: verum

G is a_partition of X

proof

then reconsider G = G as non empty a_partition of X ;
X c= union G

( 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 object 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

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

end;proof

hence
union G = X
; :: according to EQREL_1:def 4 :: thesis: for A being Subset of X st A in G holds
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in union G )

consider T being object 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

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;consider T being object 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

EqClass (a1,T) in { (EqClass (a1,S)) where S is a_partition of X : S in F }
by A8;
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;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

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

( 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 object 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

EqClass (x,T) in { (EqClass (x,S)) where S is a_partition of X : S in F }
by A11;
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;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

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

end;proof

A19:
not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty
consider T being object 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;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

proof

consider T being object 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;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

now :: thesis: ( not A meets B or A = B or A misses B )

hence
( A = B or A misses B )
; :: thesis: verumassume
A meets B
; :: thesis: ( A = B or A misses B )

then consider c being object 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;

ex A being object st

( A in EqClass (x,T) & A in EqClass (y,T) )

EqClass (x,T) meets EqClass (y,T)

end;then consider c being object 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)

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

A24: now :: thesis: for T being a_partition of X st T in F holds

c in EqClass (x,T)

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

ex A being object st

( A in EqClass (x,T) & A in EqClass (y,T) )

proof

A27:
for T being a_partition of X st T in F holds
let T be a_partition of X; :: thesis: ( T in F implies ex A being object st

( A in EqClass (x,T) & A in EqClass (y,T) ) )

assume A26: T in F ; :: thesis: ex A being object 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;( A in EqClass (x,T) & A in EqClass (y,T) ) )

assume A26: T in F ; :: thesis: ex A being object 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

EqClass (x,T) meets EqClass (y,T)

proof

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 }
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 object 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;assume T in F ; :: thesis: EqClass (x,T) meets EqClass (y,T)

then ex A being object 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

proof

{ (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 }
let A be object ; :: 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;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

proof

hence
( A = B or A misses B )
by A15, A16, A28, XBOOLE_0:def 10; :: thesis: verum
let A be object ; :: 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;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

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

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
let x be Element of X; :: thesis: EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F }

hence EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } by Def6; :: thesis: verum

end;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

not { (EqClass (x,S)) where S is a_partition of X : S in F } is empty
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;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

proof

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;
consider T being object 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;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

hence EqClass (x,G) = meet { (EqClass (x,S)) where S is a_partition of X : S in F } by Def6; :: thesis: verum