let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass z,((C '/\' D) '/\' E) = EqClass u,((C '/\' D) '/\' E) 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, E being a_partition of Y
for z, u being Element of Y st G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass z,((C '/\' D) '/\' E) = EqClass u,((C '/\' D) '/\' E) holds
EqClass u,(CompF A,G) meets EqClass z,(CompF B,G)
let A, B, C, D, E be a_partition of Y; :: thesis: for z, u being Element of Y st G is independent & G = {A,B,C,D,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass z,((C '/\' D) '/\' E) = EqClass u,((C '/\' D) '/\' E) 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,E} & A <> B & A <> C & A <> D & A <> E & B <> C & B <> D & B <> E & C <> D & C <> E & D <> E & EqClass z,((C '/\' D) '/\' E) = EqClass u,((C '/\' D) '/\' E) 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,E} and
A3: A <> B and
A4: ( A <> C & A <> D & A <> E ) and
A5: ( B <> C & B <> D & B <> E ) and
A6: ( C <> D & C <> E & D <> E ) and
A7: EqClass z,((C '/\' D) '/\' E) = EqClass u,((C '/\' D) '/\' E) ; :: 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))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A));
A8: (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . B = EqClass u,B by A3, A4, A5, A6, Th29;
A9: (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . E = EqClass u,E by A3, A4, A5, A6, Th29;
A10: (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, A4, A5, A6, Th29;
A11: (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by A3, A4, A5, A6, Th29;
A12: rng (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) = {((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . A),((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . B),((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . C),((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . D),((((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . E)} by Th31;
rng (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (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))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) or t in bool Y )
assume A13: t in rng (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) ; :: thesis: t in bool Y

now

per cases ( t = (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . A or t = (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . B or t = (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . C or t = (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . D or t = (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . E ) by A12, A13, ENUMSET1:def 3;

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

then t = EqClass z,A by A3, A4, A5, A6, Th29;
hence t in bool Y ; :: thesis: verum

end;

case t = (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . B ; :: 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))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . C ; :: thesis: t in bool Y

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

end;

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

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

end;

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

hence t in bool Y by A9; :: 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))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) as Subset-Family of Y ;
A14: dom (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) = G by A2, Th30;
for d being set st d in G holds
(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (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))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . d in d )
assume A15: d in G ; :: thesis: (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . d in d

now

per cases ( d = A or d = B or d = C or d = D or d = E ) by A2, A15, ENUMSET1:def 3;

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

(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . A = EqClass z,A by A3, A4, A5, A6, Th29;
hence (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . d in d by A16; :: thesis: verum

end;

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

(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . B = EqClass u,B by A3, A4, A5, A6, Th29;
hence (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . d in d by A17; :: thesis: verum

end;

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

(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . C = EqClass u,C by A3, A4, A5, A6, Th29;
hence (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . d in d by A18; :: thesis: verum

end;

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

(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . D = EqClass u,D by A3, A4, A5, A6, Th29;
hence (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . d in d by A19; :: thesis: verum

end;

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

(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . E = EqClass u,E by A3, A4, A5, A6, Th29;
hence (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . d in d by A20; :: thesis: verum

end;

end;

end;

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

end;

then Intersect FF <> {} by A1, A14, BVFUNC_2:def 5;
then consider m being set such that
A21: m in Intersect FF by XBOOLE_0:def 1;
A in dom (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by A2, A14, ENUMSET1:def 3;
then A22: (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . A in rng (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A23: m in meet FF by A21, SETFAM_1:def 10;
then A24: m in (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . A by A22, SETFAM_1:def 1;
D in dom (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by A2, A14, ENUMSET1:def 3;
then (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . D in rng (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A25: m in (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . D by A23, SETFAM_1:def 1;
C in dom (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by A2, A14, ENUMSET1:def 3;
then (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . C in rng (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then A26: m in (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . C by A23, SETFAM_1:def 1;
B in dom (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by A2, A14, ENUMSET1:def 3;
then (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . B in rng (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . B by A23, SETFAM_1:def 1;
then m in (EqClass u,B) /\ (EqClass u,C) by A8, A11, A26, XBOOLE_0:def 4;
then A27: m in ((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D) by A10, A25, XBOOLE_0:def 4;
E in dom (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by A2, A14, ENUMSET1:def 3;
then (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . E in rng (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) by FUNCT_1:def 5;
then m in (((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . E by A23, SETFAM_1:def 1;
then A28: m in (((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E) by A9, A27, XBOOLE_0:def 4;
set GG = EqClass u,(((B '/\' C) '/\' D) '/\' E);
set I = EqClass z,A;
EqClass u,(((B '/\' C) '/\' D) '/\' E) = (EqClass u,((B '/\' C) '/\' D)) /\ (EqClass u,E) by Th1;
then A29: EqClass u,(((B '/\' C) '/\' D) '/\' E) = ((EqClass u,(B '/\' C)) /\ (EqClass u,D)) /\ (EqClass u,E) by Th1;
(((((B .--> (EqClass u,B)) +* (C .--> (EqClass u,C))) +* (D .--> (EqClass u,D))) +* (E .--> (EqClass u,E))) +* (A .--> (EqClass z,A))) . A = EqClass z,A by A3, A4, A5, A6, Th29;
then m in ((((EqClass u,B) /\ (EqClass u,C)) /\ (EqClass u,D)) /\ (EqClass u,E)) /\ (EqClass z,A) by A24, A28, XBOOLE_0:def 4;
then (EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass z,A) <> {} by A29, Th1;
then consider p being set such that
A30: p in (EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass z,A) by XBOOLE_0:def 1;
reconsider p = p as Element of Y by A30;
set K = EqClass p,((C '/\' D) '/\' E);
A31: p in EqClass u,(((B '/\' C) '/\' D) '/\' E) by A30, XBOOLE_0:def 4;
A32: z in EqClass z,A by EQREL_1:def 8;
set L = EqClass z,((C '/\' D) '/\' E);
A33: p in EqClass p,((C '/\' D) '/\' E) by EQREL_1:def 8;
EqClass u,(((B '/\' C) '/\' D) '/\' E) = EqClass u,((B '/\' (C '/\' D)) '/\' E) by PARTIT1:16;
then EqClass u,(((B '/\' C) '/\' D) '/\' E) = EqClass u,(B '/\' ((C '/\' D) '/\' E)) by PARTIT1:16;
then EqClass u,(((B '/\' C) '/\' D) '/\' E) c= EqClass z,((C '/\' D) '/\' E) by A7, BVFUNC11:3;
then EqClass p,((C '/\' D) '/\' E) meets EqClass z,((C '/\' D) '/\' E) by A31, A33, XBOOLE_0:3;
then EqClass p,((C '/\' D) '/\' E) = EqClass z,((C '/\' D) '/\' E) by EQREL_1:50;
then z in EqClass p,((C '/\' D) '/\' E) by EQREL_1:def 8;
then A34: z in (EqClass z,A) /\ (EqClass p,((C '/\' D) '/\' E)) by A32, XBOOLE_0:def 4;
set H = EqClass z,(CompF B,G);
A '/\' ((C '/\' D) '/\' E) = (A '/\' (C '/\' D)) '/\' E by PARTIT1:16;
then A35: A '/\' ((C '/\' D) '/\' E) = ((A '/\' C) '/\' D) '/\' E by PARTIT1:16;
A36: ( p in EqClass p,((C '/\' D) '/\' E) & p in EqClass z,A ) by A30, EQREL_1:def 8, XBOOLE_0:def 4;
then p in (EqClass z,A) /\ (EqClass p,((C '/\' D) '/\' E)) by XBOOLE_0:def 4;
then ( (EqClass z,A) /\ (EqClass p,((C '/\' D) '/\' E)) in INTERSECTION A,((C '/\' D) '/\' E) & not (EqClass z,A) /\ (EqClass p,((C '/\' D) '/\' E)) in {{} } ) by SETFAM_1:def 5, TARSKI:def 1;
then A37: (EqClass z,A) /\ (EqClass p,((C '/\' D) '/\' E)) in (INTERSECTION A,((C '/\' D) '/\' E)) \ {{} } by XBOOLE_0:def 5;
CompF B,G = ((A '/\' C) '/\' D) '/\' E by A2, A3, A5, Th25;
then (EqClass z,A) /\ (EqClass p,((C '/\' D) '/\' E)) in CompF B,G by A37, A35, PARTIT1:def 4;
then A38: ( (EqClass z,A) /\ (EqClass p,((C '/\' D) '/\' E)) = EqClass z,(CompF B,G) or (EqClass z,A) /\ (EqClass p,((C '/\' D) '/\' E)) misses EqClass z,(CompF B,G) ) by EQREL_1:def 6;
z in EqClass z,(CompF B,G) by EQREL_1:def 8;
then p in EqClass z,(CompF B,G) by A36, A34, A38, XBOOLE_0:3, XBOOLE_0:def 4;
then p in (EqClass u,(((B '/\' C) '/\' D) '/\' E)) /\ (EqClass z,(CompF B,G)) by A31, XBOOLE_0:def 4;
then EqClass u,(((B '/\' C) '/\' D) '/\' E) 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, Th24; :: thesis: verum