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
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 (PARTITIONS Y); :: 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 A3, Th18;
A5: ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, Th18;
A6: ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by A3, Th18;
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 A2, Th20;
rng ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (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))) +* (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 A7, A8, ENUMSET1:def 2;

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

then t = EqClass z,A by FUNCT_7:96;
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))) . 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 A2, Th19;
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 A2, A10, ENUMSET1:def 2;

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:96;
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 A3, Th18;
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 A3, Th18;
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 A3, Th18;
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 A1, A9, BVFUNC_2:def 5;
then consider m being set 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 A2, A9, ENUMSET1:def 2;
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 5;
then A17: m in meet FF by A15, SETFAM_1:def 10;
D in dom ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) by A2, A9, 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 5;
then A18: m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . D by A17, 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, A9, 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 5;
then A19: m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . C by A17, 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, A9, 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 5;
then m in ((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (A .--> (EqClass z,A))) . B by A17, SETFAM_1:def 1;
then m in (EqClass u,B) /\ (EqClass u,C) by A4, A6, A19, XBOOLE_0:def 4;
then A20: m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D) by A5, A18, XBOOLE_0:def 4;
( ((((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 A16, A17, FUNCT_7:96, SETFAM_1:def 1;
then m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass z,A) by A20, XBOOLE_0:def 4;
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 A21, Th1; :: thesis: verum