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 holds
EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) meets EqClass z,A
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 holds
EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) meets EqClass z,A
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 holds
EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) meets EqClass z,A
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 implies EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) meets EqClass z,A )
assume that
A1: G is independent and
A2: ( 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 ) ; :: thesis: EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) meets EqClass z,A
reconsider I = EqClass z,A as set ;
reconsider GG = EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) as set ;
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));
A3: 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, Th9;
A4: (((((((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 A2, Th8;
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))) . B = EqClass u,B by A2, Th8;
A6: (((((((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 A2, Th8;
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))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A2, Th8;
A8: (((((((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 A2, Th8;
A9: (((((((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 A2, Th8;
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))) . J = EqClass u,J by A2, Th8;
A11: 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 A4, A5, A6, A7, A8, A9, A10; :: thesis: verum

end;

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, A3, ENUMSET1:def 5;
then 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))) . 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;
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, A3, ENUMSET1:def 5;
then 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))) . 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;
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, A3, ENUMSET1:def 5;
then 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))) . 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;
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, A3, ENUMSET1:def 5;
then 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))) . 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;
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, A3, ENUMSET1:def 5;
then 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))) +* (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;
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, A3, ENUMSET1:def 5;
then A17: (((((((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;
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, A3, 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))) . 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;
A19: 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 Th10;
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 A19, ENUMSET1:def 5;
hence t in bool Y by A4, A5, A6, A7, A8, A9, A10; :: 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 ;
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))) +* (A .--> (EqClass z,A)))) by A12, SETFAM_1:def 10;
Intersect FF <> {} by A1, A3, A11, BVFUNC_2:def 5;
then consider m being set such that
A21: m in Intersect FF by XBOOLE_0:def 1;
A22: ( m in EqClass z,A & m in EqClass u,B & m in EqClass u,C & m in EqClass u,D & m in EqClass u,E & m in EqClass u,F & m in EqClass u,J ) by A4, A5, A6, A7, A8, A9, A10, A12, A13, A14, A15, A16, A17, A18, A20, A21, SETFAM_1:def 1;
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 A23: 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;
m in (EqClass u,B) /\ (EqClass u,C) by A22, XBOOLE_0:def 4;
then m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D) by A22, XBOOLE_0:def 4;
then m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E) by A22, XBOOLE_0:def 4;
then m in ((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F) by A22, XBOOLE_0:def 4;
then m in (((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass u,F)) /\ (EqClass u,J) by A22, XBOOLE_0:def 4;
then m in (EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J)) /\ (EqClass z,A) by A22, A23, XBOOLE_0:def 4;
hence EqClass u,(((((B '/\' C) '/\' D) '/\' E) '/\' F) '/\' J) meets EqClass z,A by XBOOLE_0:def 7; :: thesis: verum