let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J, M being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) 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, J, M being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C, D, E, F, J, M be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) 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,F,J,M} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & A <> M & B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M & EqClass z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) 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,J,M} and
A3: ( A <> B & A <> C & A <> D & A <> E & A <> F & A <> J ) and
A4: A <> M and
A5: ( B <> C & B <> D & B <> E & B <> F & B <> J & B <> M & C <> D & C <> E & C <> F & C <> J & C <> M & D <> E & D <> F & D <> J & D <> M & E <> F & E <> J & E <> M & F <> J & F <> M & J <> M ) and
A6: EqClass z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) ; :: 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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A));
A7: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . B = EqClass u,B by A3, A5, Th65;
set HH = EqClass z,(CompF B,G);
set I = EqClass z,A;
set GG = EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M);
A8: EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(CompF A,G) by A2, A3, A4, A5, Th57;
EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = (EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J)) /\ (EqClass u,M) by Th1;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = ((EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass u,J)) /\ (EqClass u,M) by Th1;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = (((EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M) by Th1;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = ((((EqClass u,((B '/\' C) '/\' D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M) by Th1;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = (((((EqClass u,(B '/\' C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M) by Th1;
then A9: (EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) /\ (EqClass z,A) = (((((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M)) /\ (EqClass z,A) by Th1;
A10: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . A = EqClass z,A by FUNCT_7:96;
A11: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by A3, A5, Th65;
A12: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . M = EqClass u,M by A4, Lm2;
A13: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . J = EqClass u,J by A3, A5, Th65;
A14: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . F = EqClass u,F by A3, A5, Th65;
A15: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . E = EqClass u,E by A3, A5, Th65;
A16: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, A5, Th65;
A17: rng ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) = {(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . F),(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . J),(((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . M)} by Th67;
rng ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) or t in bool Y )
assume t in rng ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) ; :: thesis: t in bool Y
then ( t = ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . F or t = ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . J or t = ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . M ) by A17, ENUMSET1:def 6;
hence t in bool Y by A10, A7, A11, A16, A15, A14, A13, A12; :: 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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) as Subset-Family of Y ;
A18: dom ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) = G by A2, Th66;
then A in dom ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by A2, ENUMSET1:def 6;
then A19: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A20: Intersect FF = meet (rng ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . d in d )
assume d in G ; :: thesis: ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . d in d
then ( d = A or d = B or d = C or d = D or d = E or d = F or d = J or d = M ) by A2, ENUMSET1:def 6;
hence ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . d in d by A10, A7, A11, A16, A15, A14, A13, A12; :: thesis: verum

end;

then Intersect FF <> {} by A1, A18, BVFUNC_2:def 5;
then consider m being set such that
A21: m in Intersect FF by XBOOLE_0:def 1;
C in dom ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A22: m in EqClass u,C by A11, A20, A21, SETFAM_1:def 1;
B in dom ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,B by A7, A20, A21, SETFAM_1:def 1;
then A23: m in (EqClass u,B) /\ (EqClass u,C) by A22, XBOOLE_0:def 4;
D in dom ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,D by A16, A20, A21, SETFAM_1:def 1;
then A24: m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D) by A23, XBOOLE_0:def 4;
E in dom ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,E by A15, A20, A21, SETFAM_1:def 1;
then A25: m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E) by A24, 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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (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))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,F by A14, A20, A21, SETFAM_1:def 1;
then A26: m in ((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F) by A25, XBOOLE_0:def 4;
J in dom ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . J in rng ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,J by A13, A20, A21, SETFAM_1:def 1;
then A27: m in (((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J) by A26, XBOOLE_0:def 4;
M in dom ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by A2, A18, ENUMSET1:def 6;
then ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) . M in rng ((((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (M .--> (EqClass u,M))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in EqClass u,M by A12, A20, A21, SETFAM_1:def 1;
then A28: m in ((((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass u,M) by A27, XBOOLE_0:def 4;
m in EqClass z,A by A10, A19, A20, A21, SETFAM_1:def 1;
then (EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) /\ (EqClass z,A) <> {} by A9, A28, XBOOLE_0:def 4;
then consider p being set such that
A29: p in (EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) /\ (EqClass z,A) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A29;
reconsider K = EqClass p,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) as set ;
A30: p in EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) by A29, XBOOLE_0:def 4;
reconsider L = EqClass z,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) as set ;
A31: p in EqClass p,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) by EQREL_1:def 8;
EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(((((B '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J) '/\' M) by PARTIT1:16;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,((((B '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J) '/\' M) by PARTIT1:16;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(((B '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J) '/\' M) by PARTIT1:16;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,((B '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J)) '/\' M) by PARTIT1:16;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = EqClass u,(B '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) by PARTIT1:16;
then EqClass u,((((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) c= L by A6, BVFUNC11:3;
then K meets L by A30, A31, XBOOLE_0:3;
then K = L by EQREL_1:50;
then A32: z in K by EQREL_1:def 8;
A33: z in EqClass z,(CompF B,G) by EQREL_1:def 8;
z in EqClass z,A by EQREL_1:def 8;
then z in (EqClass z,A) /\ K by A32, XBOOLE_0:def 4;
then A34: (EqClass z,A) /\ K meets EqClass z,(CompF B,G) by A33, XBOOLE_0:3;
A35: A '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) = (A '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J)) '/\' M by PARTIT1:16
.= ((A '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J) '/\' M by PARTIT1:16
.= (((A '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J) '/\' M by PARTIT1:16
.= ((((A '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J) '/\' M by PARTIT1:16
.= (((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M by PARTIT1:16 ;
( p in K & p in EqClass z,A ) by A29, EQREL_1:def 8, XBOOLE_0:def 4;
then A36: p in (EqClass z,A) /\ K by XBOOLE_0:def 4;
then ( (EqClass z,A) /\ K in INTERSECTION A,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) & not (EqClass z,A) /\ K in {{} } ) by SETFAM_1:def 5, TARSKI:def 1;
then (EqClass z,A) /\ K in (INTERSECTION A,(((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M)) \ {{} } by XBOOLE_0:def 5;
then A37: (EqClass z,A) /\ K in A '/\' (((((C '/\' D) '/\' E) '/\' F) '/\' J) '/\' M) by PARTIT1:def 4;
CompF B,G = (((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) '/\' M by A2, A3, A4, A5, Th58;
then p in EqClass z,(CompF B,G) by A36, A37, A34, A35, EQREL_1:def 6;
hence EqClass u,(CompF A,G) meets EqClass z,(CompF B,G) by A8, A30, XBOOLE_0:3; :: thesis: verum