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
for h being Function st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)

let G be Subset of (); :: thesis: for A, B, C, D being a_partition of Y
for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)

let A, B, C, D be a_partition of Y; :: thesis: for z, u being Element of Y
for h being Function st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)

let z, u be Element of Y; :: thesis: for h being Function st G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D holds
EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)

let h be Function; :: thesis: ( G is independent & G = {A,B,C,D} & A <> B & A <> C & A <> D & B <> C & B <> D & C <> D implies EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A) )
assume that
A1: G is independent and
A2: G = {A,B,C,D} and
A3: ( A <> B & A <> C & A <> D & B <> C & B <> D & C <> D ) ; :: thesis: EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A)
set h = (((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)));
A4: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B = EqClass (u,B) by ;
A5: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . D = EqClass (u,D) by ;
A6: ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . C = EqClass (u,C) by ;
A7: 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 A8: 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
hence t in bool Y by A4; :: 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
hence t in bool Y by A6; :: 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
hence t in bool Y by A5; :: 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 ;
A9: dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) = G by ;
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 A10: 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 A11: 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 A11; :: thesis: verum
end;
suppose A12: 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 ;
hence ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d by A12; :: thesis: verum
end;
suppose A13: 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 ;
hence ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . d in d by A13; :: thesis: verum
end;
suppose A14: 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 ;
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;
end;
end;
then Intersect FF <> {} by ;
then consider m being object such that
A15: m in Intersect FF by XBOOLE_0:def 1;
A in dom ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) by ;
then A16: ((((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 A17: m in meet FF 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 A18: 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 A19: 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 m in ((((B .--> (EqClass (u,B))) +* (C .--> (EqClass (u,C)))) +* (D .--> (EqClass (u,D)))) +* (A .--> (EqClass (z,A)))) . B by ;
then m in (EqClass (u,B)) /\ (EqClass (u,C)) by ;
then A20: m in ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) by ;
( ((((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 ;
then m in (((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D))) /\ (EqClass (z,A)) by ;
then A21: ((EqClass (u,B)) /\ (EqClass (u,C))) /\ (EqClass (u,D)) meets EqClass (z,A) by XBOOLE_0:4;
EqClass (u,((B '/\' C) '/\' D)) = (EqClass (u,(B '/\' C))) /\ (EqClass (u,D)) by Th1;
hence EqClass (u,((B '/\' C) '/\' D)) meets EqClass (z,A) by ; :: thesis: verum