let Y be non empty set ; :: thesis: for G being Subset of ()
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 (); :: 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)));
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:13;
then A8: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A = EqClass (z,A) by FUNCOP_1:72;
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;
A12: C in dom (C .--> (EqClass (u,C))) by TARSKI:def 1;
not B in dom (A .--> (EqClass (z,A))) by ;
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:11;
not B in dom (C .--> (EqClass (u,C))) by ;
then (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B = (B .--> (EqClass (u,B))) . B by ;
then A14: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by FUNCOP_1:72;
not C in dom (A .--> (EqClass (z,A))) by ;
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:11;
then (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C = (C .--> (EqClass (u,C))) . C by ;
then A15: (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by FUNCOP_1:72;
A16: dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) = ({A} \/ {B}) \/ {C} by
.= {A,B} \/ {C} by ENUMSET1:1
.= {A,B,C} by ENUMSET1:3 ;
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 object ; :: 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 object 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 3;
now :: thesis: ( ( x1 = A & 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)} ) or ( x1 = B & 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)} ) or ( x1 = C & 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)} ) )
per cases ( x1 = A or x1 = B or x1 = C ) by ;
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 ; :: 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 ; :: 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 ; :: 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 object ; :: 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 :: thesis: ( ( t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A & t in bool Y ) or ( t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B & t in bool Y ) or ( t = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C & t in bool Y ) )
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 ;
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 6;
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 :: thesis: ( ( d = A & (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = B & (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d ) or ( d = C & (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . d in d ) )
per cases ( d = A or d = B or d = C ) by ;
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 ;
then consider m being object 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 ;
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 3;
then A25: Intersect FF = meet (rng (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A))))) by SETFAM_1:def 9;
C in dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) by ;
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 3;
then A26: m in (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . C by ;
B in dom (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) by ;
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 3;
then m in (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . B by ;
then A27: m in (EqClass (u,B)) /\ (EqClass (u,C)) by ;
m in (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (A .--> (EqClass (z,A)))) . A by ;
then (EqClass (u,(B '/\' C))) /\ (EqClass (z,A)) <> {} by ;
then consider p being object 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 6;
A31: p in EqClass (u,(B '/\' C)) by ;
( p in EqClass (p,C) & p in EqClass (z,A) ) by ;
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 ;
then A33: (EqClass (z,A)) /\ (EqClass (p,C)) in A '/\' C by PARTIT1:def 4;
EqClass (u,(B '/\' C)) c= EqClass (z,C) by ;
then EqClass (p,C) meets EqClass (z,C) by ;
then EqClass (p,C) = EqClass (z,C) by EQREL_1:41;
then A34: z in EqClass (p,C) by EQREL_1:def 6;
z in EqClass (z,A) by EQREL_1:def 6;
then A35: z in (EqClass (z,A)) /\ (EqClass (p,C)) by ;
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 ;
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 ; :: thesis: verum