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: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 A2, Th17;
rng ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) c= bool Y 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 dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) = G by A2, Th16;
then Intersect FF <> {} by A1, A12, BVFUNC_2:def 5;
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 A2, Th16;
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 3;
then A21: m in meet FF by A18, SETFAM_1:def 9;
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:94, 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 3;
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 3;
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 3;
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, Th15;
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, Th15;
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 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 A27, XBOOLE_0:def 4;
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 A7, A30, A28, XBOOLE_0:3;
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 A29, XBOOLE_0:def 4;
A32: ( p in EqClass (p,(C '/\' D)) & p in EqClass (z,A) ) by A27, EQREL_1:def 6, 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 4;
z in EqClass (z,(CompF (B,G))) by EQREL_1:def 6;
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