let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E, F being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C, D, E, F be a_partition of Y; :: thesis: for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let z, u be Element of Y; :: thesis: for h being Function st G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let h be Function; :: thesis: ( G is independent & G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F & EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) 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,F} and
A3: ( A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F ) and
A4: EqClass z,(((C '/\' D) '/\' E) '/\' F) = EqClass u,(((C '/\' D) '/\' E) '/\' F) ; :: 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))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A));
A5: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . A = EqClass z,A by A3, Th40;
set I = EqClass z,A;
set GG = EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F);
set H = EqClass z,(CompF B,G);
A6: A '/\' (((C '/\' D) '/\' E) '/\' F) = (A '/\' ((C '/\' D) '/\' E)) '/\' F by PARTIT1:16
.= ((A '/\' (C '/\' D)) '/\' E) '/\' F by PARTIT1:16
.= (((A '/\' C) '/\' D) '/\' E) '/\' F by PARTIT1:16 ;
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = (EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass u,F) by Th1;
then EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = ((EqClass u,((B '/\' C) '/\' D)) /\ (EqClass u,E)) /\ (EqClass u,F) by Th1;
then EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = (((EqClass u,(B '/\' C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F) by Th1;
then A7: (EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass z,A) = (((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass z,A) by Th1;
A8: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . B = EqClass u,B by A3, Th40;
A9: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . F = EqClass u,F by A3, Th40;
A10: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . E = EqClass u,E by A3, Th40;
A11: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, Th40;
A12: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by A3, Th40;
A13: rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) = {(((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . A),(((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . B),(((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . C),(((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . D),(((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . E),(((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . F)} by Th42;
rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) c= bool Y

proof

let t be set ; :: 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))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) or t in bool Y )
assume A14: t in rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) ; :: thesis: t in bool Y

now

per cases ( t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . A or t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . B or t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . C or t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . D or t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . E or t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . F ) by A13, A14, ENUMSET1:def 4;

case t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . A ; :: thesis: t in bool Y

hence t in bool Y by A5; :: thesis: verum

end;

case t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (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))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . C ; :: thesis: t in bool Y

hence t in bool Y by A12; :: thesis: verum

end;

case t = ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . D ; :: 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))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . E ; :: 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))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . F ; :: 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))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) as Subset-Family of Y ;
A15: dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) = G by A2, Th41;
then A in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by A2, ENUMSET1:def 4;
then A16: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . A in rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A17: Intersect FF = meet (rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A)))) by SETFAM_1:def 10;
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))) +* (F .--> (EqClass u,F))) +* (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))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d )
assume A18: d in G ; :: thesis: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d

now

per cases ( d = A or d = B or d = C or d = D or d = E or d = F ) by A2, A18, ENUMSET1:def 4;

case d = A ; :: thesis: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d

hence ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d by A5; :: thesis: verum

end;

case d = B ; :: thesis: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d

hence ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d by A8; :: thesis: verum

end;

case d = C ; :: thesis: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d

hence ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d by A12; :: thesis: verum

end;

case d = D ; :: thesis: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d

hence ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d by A11; :: thesis: verum

end;

case d = E ; :: thesis: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d

hence ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d by A10; :: thesis: verum

end;

case d = F ; :: thesis: ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d

hence ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d by A9; :: thesis: verum

end;

end;

end;

hence ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . d in d ; :: thesis: verum

end;

then Intersect FF <> {} by A1, A15, BVFUNC_2:def 5;
then consider m being set such that
A19: m in Intersect FF by XBOOLE_0:def 1;
D in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 4;
then ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . D in rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . D by A17, A19, SETFAM_1:def 1;
then A20: m in EqClass u,D by A3, Th40;
C in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 4;
then ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . C in rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . C by A17, A19, SETFAM_1:def 1;
then A21: m in EqClass u,C by A3, Th40;
B in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 4;
then ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . B in rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . B by A17, A19, SETFAM_1:def 1;
then m in EqClass u,B by A3, Th40;
then m in (EqClass u,B) /\ (EqClass u,C) by A21, XBOOLE_0:def 4;
then A22: m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D) by A20, XBOOLE_0:def 4;
F in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 4;
then ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . F in rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . F by A17, A19, SETFAM_1:def 1;
then A23: m in EqClass u,F by A3, Th40;
E in dom ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by A2, A15, ENUMSET1:def 4;
then ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . E in rng ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . E by A17, A19, SETFAM_1:def 1;
then m in EqClass u,E by A3, Th40;
then m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E) by A22, XBOOLE_0:def 4;
then A24: m in ((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F) by A23, XBOOLE_0:def 4;
m in ((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (A .--> (EqClass z,A))) . A by A16, A17, A19, SETFAM_1:def 1;
then m in EqClass z,A by A3, Th40;
then (EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass z,A) <> {} by A7, A24, XBOOLE_0:def 4;
then consider p being set such that
A25: p in (EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass z,A) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A25;
A26: p in EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) by A25, XBOOLE_0:def 4;
set L = EqClass z,(((C '/\' D) '/\' E) '/\' F);
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = EqClass u,(((B '/\' (C '/\' D)) '/\' E) '/\' F) by PARTIT1:16;
then EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = EqClass u,((B '/\' ((C '/\' D) '/\' E)) '/\' F) by PARTIT1:16;
then EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = EqClass u,(B '/\' (((C '/\' D) '/\' E) '/\' F)) by PARTIT1:16;
then A27: EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) c= EqClass z,(((C '/\' D) '/\' E) '/\' F) by A4, BVFUNC11:3;
A28: z in EqClass z,(CompF B,G) by EQREL_1:def 8;
set K = EqClass p,(((C '/\' D) '/\' E) '/\' F);
( p in EqClass p,(((C '/\' D) '/\' E) '/\' F) & p in EqClass z,A ) by A25, EQREL_1:def 8, XBOOLE_0:def 4;
then A29: p in (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) by XBOOLE_0:def 4;
then ( (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) in INTERSECTION A,(((C '/\' D) '/\' E) '/\' F) & not (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) in {{} } ) by SETFAM_1:def 5, TARSKI:def 1;
then (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) in (INTERSECTION A,(((C '/\' D) '/\' E) '/\' F)) \ {{} } by XBOOLE_0:def 5;
then A30: (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) in A '/\' (((C '/\' D) '/\' E) '/\' F) by PARTIT1:def 4;
p in EqClass p,(((C '/\' D) '/\' E) '/\' F) by EQREL_1:def 8;
then EqClass p,(((C '/\' D) '/\' E) '/\' F) meets EqClass z,(((C '/\' D) '/\' E) '/\' F) by A27, A26, XBOOLE_0:3;
then EqClass p,(((C '/\' D) '/\' E) '/\' F) = EqClass z,(((C '/\' D) '/\' E) '/\' F) by EQREL_1:50;
then A31: z in EqClass p,(((C '/\' D) '/\' E) '/\' F) by EQREL_1:def 8;
z in EqClass z,A by EQREL_1:def 8;
then A32: z in (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) by A31, XBOOLE_0:def 4;
CompF B,G = (((A '/\' C) '/\' D) '/\' E) '/\' F by A2, A3, Th35;
then A33: ( (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) = EqClass z,(CompF B,G) or (EqClass z,A) /\ (EqClass p,(((C '/\' D) '/\' E) '/\' F)) misses EqClass z,(CompF B,G) ) by A30, A6, EQREL_1:def 6;
EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F) = EqClass u,(CompF A,G) by A2, A3, Th34;
hence EqClass u,(CompF A,G) meets EqClass z,(CompF B,G) by A29, A26, A32, A28, A33, XBOOLE_0:3; :: thesis: verum