let Y be non empty set ; :: thesis: for G being Subset of ()
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 (); :: 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:14;
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 ;
rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) c= bool Y
proof
let t be object ; :: 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 ;
suppose t = ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . A ; :: thesis: t in bool Y
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, Th15;
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, Th15;
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, Th15;
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 ;
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:94;
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, Th15;
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, Th15;
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, Th15;
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 ;
then Intersect FF <> {} by ;
then consider m being object 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 ;
then A in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by ;
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 3;
then A21: m in meet FF by ;
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 ;
D in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by ;
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 3;
then A23: m in ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D by ;
C in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by ;
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 3;
then A24: m in ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C by ;
B in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by ;
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 3;
then A25: m in ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B by ;
( ((((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, Th15;
then A26: m in (EqClass (u,B)) /\ (EqClass (u,C)) by ;
((((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, Th15;
then m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) by ;
then m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (z,A)) by ;
then (EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (z,A)) <> {} by ;
then consider p being object 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 ;
set L = EqClass (z,(C '/\' D));
A29: z in EqClass (z,A) by EQREL_1:def 6;
EqClass (u,((B '/\' C) '/\' D)) = EqClass (u,(B '/\' (C '/\' D))) by PARTIT1:14;
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 6;
then EqClass (p,(C '/\' D)) meets EqClass (z,(C '/\' D)) by ;
then EqClass (p,(C '/\' D)) = EqClass (z,(C '/\' D)) by EQREL_1:41;
then z in EqClass (p,(C '/\' D)) by EQREL_1:def 6;
then A31: z in (EqClass (z,A)) /\ (EqClass (p,(C '/\' D))) by ;
A32: ( p in EqClass (p,(C '/\' D)) & p in EqClass (z,A) ) by ;
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 ;
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 ;
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 4;
z in EqClass (z,(CompF (B,G))) by EQREL_1:def 6;
then p in EqClass (z,(CompF (B,G))) by ;
then p in (EqClass (u,((B '/\' C) '/\' D))) /\ (EqClass (z,(CompF (B,G)))) by ;
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