let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F, J being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & EqClass z,((((C '/\' D) '/\' E) '/\' F) '/\' J) = EqClass u,((((C '/\' D) '/\' E) '/\' F) '/\' J) 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 being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E,F,J} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & EqClass z,((((C '/\' D) '/\' E) '/\' F) '/\' J) = EqClass u,((((C '/\' D) '/\' E) '/\' F) '/\' J) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C, D, E, F, J 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} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & EqClass z,((((C '/\' D) '/\' E) '/\' F) '/\' J) = EqClass u,((((C '/\' D) '/\' E) '/\' F) '/\' J) 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} & A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J & EqClass z,((((C '/\' D) '/\' E) '/\' F) '/\' J) = EqClass u,((((C '/\' D) '/\' E) '/\' F) '/\' J) 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} and
A3: ( A <> B & A <> C & A <> D & A <> E & A <> F & A <> J & B <> C & B <> D & B <> E & B <> F & B <> J & C <> D & C <> E & C <> F & C <> J & D <> E & D <> F & D <> J & E <> F & E <> J & F <> J ) and
A4: EqClass z,((((C '/\' D) '/\' E) '/\' F) '/\' J) = EqClass u,((((C '/\' D) '/\' E) '/\' F) '/\' J) ; :: 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))) +* (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))) +* (J .--> (EqClass u,J))) +* (A .--> (EqClass z,A))) . A = EqClass z,A by A3, Th52;
reconsider L = EqClass z,((((C '/\' D) '/\' E) '/\' F) '/\' J) as set ;
reconsider GG = EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) as set ;
reconsider I = EqClass z,A as set ;
GG = (EqClass u,((((B '/\' C) '/\' D) '/\' E) '/\' F)) /\ (EqClass u,J) by Th1;
then GG = ((EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass u,F)) /\ (EqClass u,J) by Th1;
then GG = (((EqClass u,((B '/\' C) '/\' D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J) by Th1;
then GG = ((((EqClass u,(B '/\' C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J) by Th1;
then A6: GG /\ I = ((((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J)) /\ (EqClass z,A) by Th1;
A7: CompF A,G = ((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by A2, A3, Th45;
reconsider HH = EqClass z,(CompF B,G) as set ;
A8: z in HH by EQREL_1:def 8;
A9: A '/\' ((((C '/\' D) '/\' E) '/\' F) '/\' J) = (A '/\' (((C '/\' D) '/\' E) '/\' F)) '/\' J by PARTIT1:16
.= ((A '/\' ((C '/\' D) '/\' E)) '/\' F) '/\' J by PARTIT1:16
.= (((A '/\' (C '/\' D)) '/\' E) '/\' F) '/\' J by PARTIT1:16
.= ((((A '/\' C) '/\' D) '/\' E) '/\' F) '/\' J by PARTIT1:16 ;
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))) +* (A .--> (EqClass z,A))) . B = EqClass u,B by A3, Th52;
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))) +* (A .--> (EqClass z,A))) . F = EqClass u,F by A3, Th52;
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))) +* (A .--> (EqClass z,A))) . E = EqClass u,E by A3, Th52;
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))) +* (A .--> (EqClass z,A))) . J = EqClass u,J by A3, Th52;
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))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, Th52;
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))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by A3, Th52;
A16: 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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (A .--> (EqClass z,A))) . J)} by Th54;
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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (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))) +* (A .--> (EqClass z,A))) . J ) by A16, ENUMSET1:def 5;
hence t in bool Y by A5, A10, A15, A14, A12, A11, A13; :: 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))) +* (A .--> (EqClass z,A))) as Subset-Family of Y ;
A17: 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))) +* (A .--> (EqClass z,A))) = G by A2, Th53;
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))) +* (A .--> (EqClass z,A))) by A2, ENUMSET1:def 5;
then A18: (((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (F .--> (EqClass u,F))) +* (J .--> (EqClass u,J))) +* (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))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A19: 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))) +* (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))) +* (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))) +* (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))) +* (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 ) by A2, ENUMSET1:def 5;
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))) +* (A .--> (EqClass z,A))) . d in d by A5, A10, A15, A14, A12, A11, A13; :: thesis: verum

end;

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