let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) 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 being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C, D be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) 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} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D & EqClass z,(C '/\' D) = EqClass u,(C '/\' D) 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} and
A3: A <> B and
A4: ( A <> C & A <> D ) and
A5: ( B <> C & B <> D ) and
A6: C <> D and
A7: EqClass z,(C '/\' D) = EqClass u,(C '/\' D) ; :: 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))) +* (A .--> (EqClass z,A));
set H = EqClass z,(CompF B,G);
A8: A '/\' (C '/\' D) = (A '/\' C) '/\' D by PARTIT1:16;
A9: rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) = {(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . A),(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B),(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C),(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D)} by A2, Th20;
rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (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))) +* (A .--> (EqClass z,A))) or t in bool Y )
assume A10: t in rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) ; :: thesis: t in bool Y

per cases ( t = ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . A or t = ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B or t = ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C or t = ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D ) by A9, A10, ENUMSET1:def 2;

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

then t = EqClass z,A by FUNCT_7:96;
hence t in bool Y ; :: thesis: verum

end;

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

then t = EqClass u,B by A3, A4, A5, A6, Th18;
hence t in bool Y ; :: thesis: verum

end;

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

then t = EqClass u,C by A3, A4, A5, A6, Th18;
hence t in bool Y ; :: thesis: verum

end;

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

then t = EqClass u,D by A3, A4, A5, A6, Th18;
hence t in bool Y ; :: thesis: verum

end;

end;

end;

then reconsider FF = rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) as Subset-Family of Y ;
set I = EqClass z,A;
set GG = EqClass u,((B '/\' C) '/\' D);
A11: EqClass u,((B '/\' C) '/\' D) = (EqClass u,(B '/\' C)) /\ (EqClass u,D) by Th1;
A12: for d being set st d in G holds
((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (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))) +* (A .--> (EqClass z,A))) . d in d )
assume A13: d in G ; :: thesis: ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . d in d

per cases ( d = A or d = B or d = C or d = D ) by A2, A13, ENUMSET1:def 2;

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

((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . A = EqClass z,A by FUNCT_7:96;
hence ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . d in d by A14; :: thesis: verum

end;

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

((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B = EqClass u,B by A3, A4, A5, A6, Th18;
hence ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . d in d by A15; :: thesis: verum

end;

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

((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by A3, A4, A5, A6, Th18;
hence ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . d in d by A16; :: thesis: verum

end;

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

((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, A4, A5, A6, Th18;
hence ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . d in d by A17; :: thesis: verum

end;

end;

end;

dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) = G by A2, Th19;
then Intersect FF <> {} by A1, A12, BVFUNC_2:def 5;
then consider m being set such that
A18: m in Intersect FF by XBOOLE_0:def 1;
A19: dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) = G by A2, Th19;
then A in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by A2, ENUMSET1:def 2;
then A20: ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . A in rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A21: m in meet FF by A18, SETFAM_1:def 10;
then A22: ( ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . A = EqClass z,A & m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . A ) by A20, FUNCT_7:96, SETFAM_1:def 1;
D in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by A2, A19, ENUMSET1:def 2;
then ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D in rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A23: m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D by A21, SETFAM_1:def 1;
C in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by A2, A19, ENUMSET1:def 2;
then ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C in rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A24: m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C by A21, SETFAM_1:def 1;
B in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by A2, A19, ENUMSET1:def 2;
then ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B in rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A25: m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B by A21, SETFAM_1:def 1;
( ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B = EqClass u,B & ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C = EqClass u,C ) by A3, A4, A5, A6, Th18;
then A26: m in (EqClass u,B) /\ (EqClass u,C) by A25, A24, XBOOLE_0:def 4;
((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, A4, A5, A6, Th18;
then m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D) by A23, A26, XBOOLE_0:def 4;
then m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass z,A) by A22, XBOOLE_0:def 4;
then (EqClass u,((B '/\' C) '/\' D)) /\ (EqClass z,A) <> {} by A11, Th1;
then consider p being set such that
A27: p in (EqClass u,((B '/\' C) '/\' D)) /\ (EqClass z,A) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A27;
set K = EqClass p,(C '/\' D);
A28: p in EqClass u,((B '/\' C) '/\' D) by A27, XBOOLE_0:def 4;
set L = EqClass z,(C '/\' D);
A29: z in EqClass z,A by EQREL_1:def 8;
EqClass u,((B '/\' C) '/\' D) = EqClass u,(B '/\' (C '/\' D)) by PARTIT1:16;
then A30: EqClass u,((B '/\' C) '/\' D) c= EqClass u,(C '/\' D) by BVFUNC11:3;
p in EqClass p,(C '/\' D) by EQREL_1:def 8;
then EqClass p,(C '/\' D) meets EqClass z,(C '/\' D) by A7, A30, A28, XBOOLE_0:3;
then EqClass p,(C '/\' D) = EqClass z,(C '/\' D) by EQREL_1:50;
then z in EqClass p,(C '/\' D) by EQREL_1:def 8;
then A31: z in (EqClass z,A) /\ (EqClass p,(C '/\' D)) by A29, XBOOLE_0:def 4;
A32: ( p in EqClass p,(C '/\' D) & p in EqClass z,A ) by A27, EQREL_1:def 8, XBOOLE_0:def 4;
then p in (EqClass z,A) /\ (EqClass p,(C '/\' D)) by XBOOLE_0:def 4;
then ( (EqClass z,A) /\ (EqClass p,(C '/\' D)) in INTERSECTION A,(C '/\' D) & not (EqClass z,A) /\ (EqClass p,(C '/\' D)) in {{} } ) by SETFAM_1:def 5, TARSKI:def 1;
then A33: (EqClass z,A) /\ (EqClass p,(C '/\' D)) in (INTERSECTION A,(C '/\' D)) \ {{} } by XBOOLE_0:def 5;
CompF B,G = (A '/\' C) '/\' D by A2, A3, A5, Th8;
then (EqClass z,A) /\ (EqClass p,(C '/\' D)) in CompF B,G by A33, A8, PARTIT1:def 4;
then A34: ( (EqClass z,A) /\ (EqClass p,(C '/\' D)) = EqClass z,(CompF B,G) or (EqClass z,A) /\ (EqClass p,(C '/\' D)) misses EqClass z,(CompF B,G) ) by EQREL_1:def 6;
z in EqClass z,(CompF B,G) by EQREL_1:def 8;
then p in EqClass z,(CompF B,G) by A32, A31, A34, XBOOLE_0:3, XBOOLE_0:def 4;
then p in (EqClass u,((B '/\' C) '/\' D)) /\ (EqClass z,(CompF B,G)) by A28, XBOOLE_0:def 4;
then EqClass u,((B '/\' C) '/\' D) 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, Th7; :: thesis: verum