let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C} & A <> B & B <> C & C <> A & EqClass z,C = EqClass u,C holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C} & A <> B & B <> C & C <> A & EqClass z,C = EqClass u,C holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C} & A <> B & B <> C & C <> A & EqClass z,C = EqClass u,C 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} & A <> B & B <> C & C <> A & EqClass z,C = EqClass u,C implies EqClass u,(CompF A,G) meets EqClass z,(CompF B,G) )
assume that
A1: G is independent and
A2: G = {A,B,C} and
A3: A <> B and
A4: B <> C and
A5: C <> A and
A6: EqClass z,C = EqClass u,C ; :: thesis: EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
set h = ((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A));
A7: dom (A .--> (EqClass z,A)) = {A} by FUNCOP_1:19;
then A in dom (A .--> (EqClass z,A)) by TARSKI:def 1;
then (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A = (A .--> (EqClass z,A)) . A by FUNCT_4:14;
then A8: (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A = EqClass z,A by FUNCOP_1:87;
set H = EqClass z,(CompF B,G);
set I = EqClass z,A;
set GG = EqClass u,(B '/\' C);
A9: (EqClass u,(B '/\' C)) /\ (EqClass z,A) = ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass z,A) by Th1;
dom ((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) = (dom (B .--> (EqClass u,B))) \/ (dom (C .--> (EqClass u,C))) by FUNCT_4:def 1;
then A10: dom (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) = ((dom (B .--> (EqClass u,B))) \/ (dom (C .--> (EqClass u,C)))) \/ (dom (A .--> (EqClass z,A))) by FUNCT_4:def 1;
A11: dom (C .--> (EqClass u,C)) = {C} by FUNCOP_1:19;
then A12: C in dom (C .--> (EqClass u,C)) by TARSKI:def 1;
not B in dom (A .--> (EqClass z,A)) by A3, A7, TARSKI:def 1;
then A13: (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B = ((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) . B by FUNCT_4:12;
not B in dom (C .--> (EqClass u,C)) by A4, A11, TARSKI:def 1;
then (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B = (B .--> (EqClass u,B)) . B by A13, FUNCT_4:12;
then A14: (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B = EqClass u,B by FUNCOP_1:87;
not C in dom (A .--> (EqClass z,A)) by A5, A7, TARSKI:def 1;
then (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C = ((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) . C by FUNCT_4:12;
then (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C = (C .--> (EqClass u,C)) . C by A12, FUNCT_4:14;
then A15: (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by FUNCOP_1:87;
dom (B .--> (EqClass u,B)) = {B} by FUNCOP_1:19;
then A16: dom (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) = ({A} \/ {B}) \/ {C} by A10, A11, A7, XBOOLE_1:4
.= {A,B} \/ {C} by ENUMSET1:41
.= {A,B,C} by ENUMSET1:43 ;
A17: rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) c= {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)}

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) or t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)} )
assume t in rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) ; :: thesis: t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)}
then consider x1 being set such that
A18: x1 in dom (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) and
A19: t = (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . x1 by FUNCT_1:def 5;

now

per cases ( x1 = A or x1 = B or x1 = C ) by A16, A18, ENUMSET1:def 1;

case x1 = A ; :: thesis: t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)}

hence t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)} by A19, ENUMSET1:def 1; :: thesis: verum

end;

case x1 = B ; :: thesis: t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)}

hence t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)} by A19, ENUMSET1:def 1; :: thesis: verum

end;

case x1 = C ; :: thesis: t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)}

hence t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)} by A19, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

hence t in {((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B),((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C)} ; :: thesis: verum

end;

rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (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))) +* (A .--> (EqClass z,A))) or t in bool Y )
assume A20: t in rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) ; :: thesis: t in bool Y

now

per cases ( t = (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A or t = (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B or t = (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C ) by A17, A20, ENUMSET1:def 1;

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

hence t in bool Y by A8; :: thesis: verum

end;

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

hence t in bool Y by A14; :: thesis: verum

end;

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

hence t in bool Y by A15; :: thesis: verum

end;

end;

end;

hence t in bool Y ; :: thesis: verum

end;

then reconsider FF = rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) as Subset-Family of Y ;
A21: z in EqClass z,(CompF B,G) by EQREL_1:def 8;
for d being set st d in G holds
(((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (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))) +* (A .--> (EqClass z,A))) . d in d )
assume A22: d in G ; :: thesis: (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . d in d

now

per cases ( d = A or d = B or d = C ) by A2, A22, ENUMSET1:def 1;

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

hence (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . d in d by A8; :: thesis: verum

end;

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

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

end;

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

hence (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . d in d by A15; :: thesis: verum

end;

end;

end;

hence (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . d in d ; :: thesis: verum

end;

then Intersect FF <> {} by A1, A2, A16, BVFUNC_2:def 5;
then consider m being set such that
A23: m in Intersect FF by XBOOLE_0:def 1;
A in dom (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) by A16, ENUMSET1:def 1;
then A24: (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A in rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A25: Intersect FF = meet (rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A)))) by SETFAM_1:def 10;
C in dom (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) by A16, ENUMSET1:def 1;
then (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C in rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A26: m in (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . C by A25, A23, SETFAM_1:def 1;
B in dom (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) by A16, ENUMSET1:def 1;
then (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B in rng (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . B by A25, A23, SETFAM_1:def 1;
then A27: m in (EqClass u,B) /\ (EqClass u,C) by A14, A15, A26, XBOOLE_0:def 4;
m in (((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (A .--> (EqClass z,A))) . A by A24, A25, A23, SETFAM_1:def 1;
then (EqClass u,(B '/\' C)) /\ (EqClass z,A) <> {} by A8, A9, A27, XBOOLE_0:def 4;
then consider p being set such that
A28: p in (EqClass u,(B '/\' C)) /\ (EqClass z,A) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A28;
set K = EqClass p,C;
A29: (EqClass z,A) /\ (EqClass p,C) in INTERSECTION A,C by SETFAM_1:def 5;
set L = EqClass z,C;
A30: p in EqClass p,C by EQREL_1:def 8;
A31: p in EqClass u,(B '/\' C) by A28, XBOOLE_0:def 4;
( p in EqClass p,C & p in EqClass z,A ) by A28, EQREL_1:def 8, XBOOLE_0:def 4;
then A32: p in (EqClass z,A) /\ (EqClass p,C) by XBOOLE_0:def 4;
then not (EqClass z,A) /\ (EqClass p,C) in {{} } by TARSKI:def 1;
then (EqClass z,A) /\ (EqClass p,C) in (INTERSECTION A,C) \ {{} } by A29, XBOOLE_0:def 5;
then A33: (EqClass z,A) /\ (EqClass p,C) in A '/\' C by PARTIT1:def 4;
EqClass u,(B '/\' C) c= EqClass z,C by A6, BVFUNC11:3;
then EqClass p,C meets EqClass z,C by A31, A30, XBOOLE_0:3;
then EqClass p,C = EqClass z,C by EQREL_1:50;
then A34: z in EqClass p,C by EQREL_1:def 8;
z in EqClass z,A by EQREL_1:def 8;
then A35: z in (EqClass z,A) /\ (EqClass p,C) by A34, XBOOLE_0:def 4;
CompF B,G = A '/\' C by A2, A3, A4, Th5;
then A36: ( (EqClass z,A) /\ (EqClass p,C) = EqClass z,(CompF B,G) or (EqClass z,A) /\ (EqClass p,C) misses EqClass z,(CompF B,G) ) by A33, EQREL_1:def 6;
EqClass u,(B '/\' C) = EqClass u,(CompF A,G) by A2, A3, A5, Th4;
hence EqClass u,(CompF A,G) meets EqClass z,(CompF B,G) by A32, A31, A35, A21, A36, XBOOLE_0:3; :: thesis: verum