let Y be non empty set ; :: thesis: for G being Subset of ()
for A, B, C, D, E being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass (z,((C '/\' D) '/\' E)) = EqClass (u,((C '/\' D) '/\' E)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

let G be Subset of (); :: thesis: for A, B, C, D, E being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass (z,((C '/\' D) '/\' E)) = EqClass (u,((C '/\' D) '/\' E)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

let A, B, C, D, E be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass (z,((C '/\' D) '/\' E)) = EqClass (u,((C '/\' D) '/\' E)) holds
EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))

let z, u be Element of Y; :: thesis: ( G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass (z,((C '/\' D) '/\' E)) = EqClass (u,((C '/\' D) '/\' E)) implies EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G))) )
assume that
A1: G is independent and
A2: G = {A,B,C,D,E} and
A3: A <> B and
A4: ( A <> C & A <> D & A <> E ) and
A5: ( B <> C & B <> D & B <> E ) and
A6: ( C <> D & C <> E & D <> E ) and
A7: EqClass (z,((C '/\' D) '/\' E)) = EqClass (u,((C '/\' D) '/\' E)) ; :: thesis: EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G)))
set h = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)));
A8: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by A3, A4, A5, A6, Th26;
A9: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E) by A3, A4, A5, A6, Th26;
A10: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by A3, A4, A5, A6, Th26;
A11: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by A3, A4, A5, A6, Th26;
A12: rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) = {((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A),((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B),((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C),((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D),((((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E)} by Th28;
rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) c= bool Y
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) or t in bool Y )
assume A13: t in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) ; :: thesis: t in bool Y
now :: thesis: ( ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A & t in bool Y ) or ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B & t in bool Y ) or ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C & t in bool Y ) or ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D & t in bool Y ) or ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E & t in bool Y ) )
per cases ( t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A or t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B or t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C or t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D or t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E ) by ;
case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A ; :: thesis: t in bool Y
then t = EqClass (z,A) by A3, A4, A5, A6, Th26;
hence t in bool Y ; :: thesis: verum
end;
case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B ; :: thesis: t in bool Y
hence t in bool Y by A8; :: thesis: verum
end;
case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C ; :: thesis: t in bool Y
hence t in bool Y by A11; :: thesis: verum
end;
case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D ; :: thesis: t in bool Y
hence t in bool Y by A10; :: thesis: verum
end;
case t = (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E ; :: thesis: t in bool Y
hence t in bool Y by A9; :: thesis: verum
end;
end;
end;
hence t in bool Y ; :: thesis: verum
end;
then reconsider FF = rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) as Subset-Family of Y ;
A14: dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) = G by ;
for d being set st d in G holds
(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d
proof
let d be set ; :: thesis: ( d in G implies (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d )
assume A15: d in G ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d
now :: thesis: ( ( d = A & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = B & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = C & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = D & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = E & (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ) )
per cases ( d = A or d = B or d = C or d = D or d = E ) by ;
case A16: d = A ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d
(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by A3, A4, A5, A6, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A16; :: thesis: verum
end;
case A17: d = B ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d
(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by A3, A4, A5, A6, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A17; :: thesis: verum
end;
case A18: d = C ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d
(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by A3, A4, A5, A6, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A18; :: thesis: verum
end;
case A19: d = D ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d
(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by A3, A4, A5, A6, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A19; :: thesis: verum
end;
case A20: d = E ; :: thesis: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d
(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E = EqClass (u,E) by A3, A4, A5, A6, Th26;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d by A20; :: thesis: verum
end;
end;
end;
hence (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . d in d ; :: thesis: verum
end;
then Intersect FF <> {} by ;
then consider m being object such that
A21: m in Intersect FF by XBOOLE_0:def 1;
A in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by ;
then A22: (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A23: m in meet FF by ;
then A24: m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A by ;
D in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by ;
then (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A25: m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . D by ;
C in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by ;
then (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then A26: m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . C by ;
B in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by ;
then (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . B by ;
then m in (EqClass (u,B)) /\ (EqClass (u,C)) by ;
then A27: m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) by ;
E in dom (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by ;
then (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E in rng (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) by FUNCT_1:def 3;
then m in (((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . E by ;
then A28: m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E)) by ;
set GG = EqClass (u,(((B '/\' C) '/\' D) '/\' E));
set I = EqClass (z,A);
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) = (EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (u,E)) by Th1;
then A29: EqClass (u,(((B '/\' C) '/\' D) '/\' E)) = ((EqClass (u,(B '/\' C))) /\ (EqClass (u,D))) /\ (EqClass (u,E)) by Th1;
(((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (E .--> (EqClass (u,E)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by A3, A4, A5, A6, Th26;
then m in ((((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (u,E))) /\ (EqClass (z,A)) by ;
then (EqClass (u,(((B '/\' C) '/\' D) '/\' E))) /\ (EqClass (z,A)) <> {} by ;
then consider p being object such that
A30: p in (EqClass (u,(((B '/\' C) '/\' D) '/\' E))) /\ (EqClass (z,A)) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A30;
set K = EqClass (p,((C '/\' D) '/\' E));
A31: p in EqClass (u,(((B '/\' C) '/\' D) '/\' E)) by ;
A32: z in EqClass (z,A) by EQREL_1:def 6;
set L = EqClass (z,((C '/\' D) '/\' E));
A33: p in EqClass (p,((C '/\' D) '/\' E)) by EQREL_1:def 6;
EqClass (u,(((B '/\' C) '/\' D) '/\' E)) = EqClass (u,((B '/\' (C '/\' D)) '/\' E)) by PARTIT1:14;
then EqClass (u,(((B '/\' C) '/\' D) '/\' E)) = EqClass (u,(B '/\' ((C '/\' D) '/\' E))) by PARTIT1:14;
then EqClass (u,(((B '/\' C) '/\' D) '/\' E)) c= EqClass (z,((C '/\' D) '/\' E)) by ;
then EqClass (p,((C '/\' D) '/\' E)) meets EqClass (z,((C '/\' D) '/\' E)) by ;
then EqClass (p,((C '/\' D) '/\' E)) = EqClass (z,((C '/\' D) '/\' E)) by EQREL_1:41;
then z in EqClass (p,((C '/\' D) '/\' E)) by EQREL_1:def 6;
then A34: z in (EqClass (z,A)) /\ (EqClass (p,((C '/\' D) '/\' E))) by ;
set H = EqClass (z,(CompF (B,G)));
A '/\' ((C '/\' D) '/\' E) = (A '/\' (C '/\' D)) '/\' E by PARTIT1:14;
then A35: A '/\' ((C '/\' D) '/\' E) = ((A '/\' C) '/\' D) '/\' E by PARTIT1:14;
A36: ( p in EqClass (p,((C '/\' D) '/\' E)) & p in EqClass (z,A) ) by ;
then p in (EqClass (z,A)) /\ (EqClass (p,((C '/\' D) '/\' E))) by XBOOLE_0:def 4;
then ( (EqClass (z,A)) /\ (EqClass (p,((C '/\' D) '/\' E))) in INTERSECTION (A,((C '/\' D) '/\' E)) & not (EqClass (z,A)) /\ (EqClass (p,((C '/\' D) '/\' E))) in ) by ;
then A37: (EqClass (z,A)) /\ (EqClass (p,((C '/\' D) '/\' E))) in (INTERSECTION (A,((C '/\' D) '/\' E))) \ by XBOOLE_0:def 5;
CompF (B,G) = ((A '/\' C) '/\' D) '/\' E by A2, A3, A5, Th22;
then (EqClass (z,A)) /\ (EqClass (p,((C '/\' D) '/\' E))) in CompF (B,G) by ;
then A38: ( (EqClass (z,A)) /\ (EqClass (p,((C '/\' D) '/\' E))) = EqClass (z,(CompF (B,G))) or (EqClass (z,A)) /\ (EqClass (p,((C '/\' D) '/\' E))) misses EqClass (z,(CompF (B,G))) ) by EQREL_1:def 4;
z in EqClass (z,(CompF (B,G))) by EQREL_1:def 6;
then p in EqClass (z,(CompF (B,G))) by ;
then p in (EqClass (u,(((B '/\' C) '/\' D) '/\' E))) /\ (EqClass (z,(CompF (B,G)))) by ;
then EqClass (u,(((B '/\' C) '/\' D) '/\' E)) meets EqClass (z,(CompF (B,G))) by XBOOLE_0:4;
hence EqClass (u,(CompF (A,G))) meets EqClass (z,(CompF (B,G))) by A2, A3, A4, Th21; :: thesis: verum