let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D, E, F being a_partition of Y st G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF (A,G) = (((B '/\' C) '/\' D) '/\' E) '/\' F
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D, E, F being a_partition of Y st G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F holds
CompF (A,G) = (((B '/\' C) '/\' D) '/\' E) '/\' F
let A, B, C, D, E, F be a_partition of Y; :: thesis: ( G = {A,B,C,D,E,F} & A <> B & A <> C & A <> D & A <> E & A <> F & B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F implies CompF (A,G) = (((B '/\' C) '/\' D) '/\' E) '/\' F )
assume that
A1: G = {A,B,C,D,E,F} and
A2: A <> B and
A3: A <> C and
A4: ( A <> D & A <> E ) and
A5: A <> F and
A6: ( B <> C & B <> D & B <> E & B <> F & C <> D & C <> E & C <> F & D <> E & D <> F & E <> F ) ; :: thesis: CompF (A,G) = (((B '/\' C) '/\' D) '/\' E) '/\' F
A7: G \ {A} = ({A} \/ {B,C,D,E,F}) \ {A} by A1, ENUMSET1:11
.= ({A} \ {A}) \/ ({B,C,D,E,F} \ {A}) by XBOOLE_1:42 ;
A8: not F in {A} by A5, TARSKI:def 1;
A9: ( not D in {A} & not E in {A} ) by A4, TARSKI:def 1;
A10: not C in {A} by A3, TARSKI:def 1;
A11: not B in {A} by A2, TARSKI:def 1;
A in {A} by TARSKI:def 1;
then A12: {A} \ {A} = {} by ZFMISC_1:60;
A13: {B,C,D,E,F} \ {A} = ({B} \/ {C,D,E,F}) \ {A} by ENUMSET1:7
.= ({B} \ {A}) \/ ({C,D,E,F} \ {A}) by XBOOLE_1:42
.= {B} \/ ({C,D,E,F} \ {A}) by A11, ZFMISC_1:59
.= {B} \/ (({C} \/ {D,E,F}) \ {A}) by ENUMSET1:4
.= {B} \/ (({C} \ {A}) \/ ({D,E,F} \ {A})) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ (({D,E} \/ {F}) \ {A})) by ENUMSET1:3
.= {B} \/ (({C} \ {A}) \/ (({D,E} \ {A}) \/ ({F} \ {A}))) by XBOOLE_1:42
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ ({F} \ {A}))) by A9, ZFMISC_1:63
.= {B} \/ (({C} \ {A}) \/ ({D,E} \/ {F})) by A8, ZFMISC_1:59
.= {B} \/ ({C} \/ ({D,E} \/ {F})) by A10, ZFMISC_1:59
.= {B} \/ ({C} \/ {D,E,F}) by ENUMSET1:3
.= {B} \/ {C,D,E,F} by ENUMSET1:4
.= {B,C,D,E,F} by ENUMSET1:7 ;
A14: (((B '/\' C) '/\' D) '/\' E) '/\' F c= '/\' (G \ {A})
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (((B '/\' C) '/\' D) '/\' E) '/\' F or x in '/\' (G \ {A}) )
reconsider xx = x as set by TARSKI:1;
assume A15: x in (((B '/\' C) '/\' D) '/\' E) '/\' F ; :: thesis: x in '/\' (G \ {A})
then A16: x <> {} by EQREL_1:def 4;
x in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ {{}} by A15, PARTIT1:def 4;
then consider bcde, f being set such that
A17: bcde in ((B '/\' C) '/\' D) '/\' E and
A18: f in F and
A19: x = bcde /\ f by SETFAM_1:def 5;
bcde in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}} by A17, PARTIT1:def 4;
then consider bcd, e being set such that
A20: bcd in (B '/\' C) '/\' D and
A21: e in E and
A22: bcde = bcd /\ e by SETFAM_1:def 5;
bcd in (INTERSECTION ((B '/\' C),D)) \ {{}} by A20, PARTIT1:def 4;
then consider bc, d being set such that
A23: bc in B '/\' C and
A24: d in D and
A25: bcd = bc /\ d by SETFAM_1:def 5;
bc in (INTERSECTION (B,C)) \ {{}} by A23, PARTIT1:def 4;
then consider b, c being set such that
A26: b in B and
A27: c in C and
A28: bc = b /\ c by SETFAM_1:def 5;
set h = ((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f);
A29: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B = b by A6, Th26;
A30: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E = e by A6, Th26;
A31: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F = f by A6, Th26;
A32: dom (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) = {F,B,C,D,E} by Th27
.= {F} \/ {B,C,D,E} by ENUMSET1:7
.= {B,C,D,E,F} by ENUMSET1:10 ;
then A33: C in dom (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by ENUMSET1:def 3;
A34: F in dom (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A32, ENUMSET1:def 3;
A35: E in dom (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A32, ENUMSET1:def 3;
A36: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C = c by A6, Th26;
A37: rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) c= {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)}
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) or t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} )
assume t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) ; :: thesis: t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)}
then consider x1 being object such that
A38: x1 in dom (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) and
A39: t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . x1 by FUNCT_1:def 3;
now :: thesis: ( ( x1 = D & t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} ) or ( x1 = B & t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} ) or ( x1 = C & t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} ) or ( x1 = E & t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} ) or ( x1 = F & t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} ) )
per cases ( x1 = D or x1 = B or x1 = C or x1 = E or x1 = F ) by A32, A38, ENUMSET1:def 3;
case x1 = D ; :: thesis: t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)}
hence t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} by A39, ENUMSET1:def 3; :: thesis: verum
end;
case x1 = B ; :: thesis: t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)}
hence t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} by A39, ENUMSET1:def 3; :: thesis: verum
end;
case x1 = C ; :: thesis: t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)}
hence t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} by A39, ENUMSET1:def 3; :: thesis: verum
end;
case x1 = E ; :: thesis: t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)}
hence t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} by A39, ENUMSET1:def 3; :: thesis: verum
end;
case x1 = F ; :: thesis: t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)}
hence t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} by A39, ENUMSET1:def 3; :: thesis: verum
end;
end;
end;
hence t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} ; :: thesis: verum
end;
A40: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D = d by A6, Th26;
rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) c= bool Y
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) or t in bool Y )
assume A41: t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) ; :: thesis: t in bool Y
now :: thesis: ( ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D & t in bool Y ) or ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B & t in bool Y ) or ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C & t in bool Y ) or ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E & t in bool Y ) or ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F & t in bool Y ) )
per cases ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D or t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B or t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C or t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E or t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F ) by A37, A41, ENUMSET1:def 3;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D ; :: thesis: t in bool Y
hence t in bool Y by A24, A40; :: thesis: verum
end;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B ; :: thesis: t in bool Y
hence t in bool Y by A26, A29; :: thesis: verum
end;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C ; :: thesis: t in bool Y
hence t in bool Y by A27, A36; :: thesis: verum
end;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E ; :: thesis: t in bool Y
hence t in bool Y by A21, A30; :: thesis: verum
end;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F ; :: thesis: t in bool Y
hence t in bool Y by A18, A31; :: thesis: verum
end;
end;
end;
hence t in bool Y ; :: thesis: verum
end;
then reconsider FF = rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) as Subset-Family of Y ;
A42: D in dom (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A32, ENUMSET1:def 3;
then (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by FUNCT_1:def 3;
then A43: Intersect FF = meet (rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f))) by SETFAM_1:def 9;
A44: B in dom (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A32, ENUMSET1:def 3;
{((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} c= rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f))
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} or t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) )
assume A45: t in {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} ; :: thesis: t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f))
now :: thesis: ( ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D & t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) ) or ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B & t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) ) or ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C & t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) ) or ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E & t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) ) or ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F & t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) ) )
per cases ( t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D or t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B or t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C or t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E or t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F ) by A45, ENUMSET1:def 3;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D ; :: thesis: t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f))
hence t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A42, FUNCT_1:def 3; :: thesis: verum
end;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B ; :: thesis: t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f))
hence t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A44, FUNCT_1:def 3; :: thesis: verum
end;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C ; :: thesis: t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f))
hence t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A33, FUNCT_1:def 3; :: thesis: verum
end;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E ; :: thesis: t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f))
hence t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A35, FUNCT_1:def 3; :: thesis: verum
end;
case t = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F ; :: thesis: t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f))
hence t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A34, FUNCT_1:def 3; :: thesis: verum
end;
end;
end;
hence t in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) ; :: thesis: verum
end;
then A46: rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) = {((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E),((((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F)} by A37, XBOOLE_0:def 10;
A47: xx c= Intersect FF
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in xx or u in Intersect FF )
assume A48: u in xx ; :: thesis: u in Intersect FF
for y being set st y in FF holds
u in y
proof
let y be set ; :: thesis: ( y in FF implies u in y )
assume A49: y in FF ; :: thesis: u in y
now :: thesis: ( ( y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D & u in y ) or ( y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B & u in y ) or ( y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C & u in y ) or ( y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E & u in y ) or ( y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F & u in y ) )
per cases ( y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D or y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B or y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C or y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E or y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F ) by A37, A49, ENUMSET1:def 3;
case A50: y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D ; :: thesis: u in y
u in (d /\ ((b /\ c) /\ e)) /\ f by A19, A22, A25, A28, A48, XBOOLE_1:16;
then A51: u in d /\ (((b /\ c) /\ e) /\ f) by XBOOLE_1:16;
y = d by A6, A50, Th26;
hence u in y by A51, XBOOLE_0:def 4; :: thesis: verum
end;
case A52: y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B ; :: thesis: u in y
u in ((c /\ (d /\ b)) /\ e) /\ f by A19, A22, A25, A28, A48, XBOOLE_1:16;
then u in (c /\ ((d /\ b) /\ e)) /\ f by XBOOLE_1:16;
then u in (c /\ ((d /\ e) /\ b)) /\ f by XBOOLE_1:16;
then u in c /\ (((d /\ e) /\ b) /\ f) by XBOOLE_1:16;
then u in c /\ ((d /\ e) /\ (f /\ b)) by XBOOLE_1:16;
then u in (c /\ (d /\ e)) /\ (f /\ b) by XBOOLE_1:16;
then A53: u in ((c /\ (d /\ e)) /\ f) /\ b by XBOOLE_1:16;
y = b by A6, A52, Th26;
hence u in y by A53, XBOOLE_0:def 4; :: thesis: verum
end;
case A54: y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C ; :: thesis: u in y
u in ((c /\ (b /\ d)) /\ e) /\ f by A19, A22, A25, A28, A48, XBOOLE_1:16;
then u in (c /\ ((b /\ d) /\ e)) /\ f by XBOOLE_1:16;
then A55: u in c /\ (((b /\ d) /\ e) /\ f) by XBOOLE_1:16;
y = c by A6, A54, Th26;
hence u in y by A55, XBOOLE_0:def 4; :: thesis: verum
end;
case y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E ; :: thesis: u in y
then A56: y = e by A6, Th26;
u in (((b /\ c) /\ d) /\ f) /\ e by A19, A22, A25, A28, A48, XBOOLE_1:16;
hence u in y by A56, XBOOLE_0:def 4; :: thesis: verum
end;
case y = (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F ; :: thesis: u in y
hence u in y by A19, A31, A48, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
hence u in y ; :: thesis: verum
end;
then u in meet FF by A46, SETFAM_1:def 1;
hence u in Intersect FF by A46, SETFAM_1:def 9; :: thesis: verum
end;
A57: for p being set st p in G \ {A} holds
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p
proof
let p be set ; :: thesis: ( p in G \ {A} implies (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p )
assume A58: p in G \ {A} ; :: thesis: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p
now :: thesis: ( ( p = D & (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p ) or ( p = B & (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p ) or ( p = C & (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p ) or ( p = E & (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p ) or ( p = F & (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p ) )
per cases ( p = D or p = B or p = C or p = E or p = F ) by A7, A12, A58, ENUMSET1:def 3;
case p = D ; :: thesis: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p
hence (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p by A6, A24, Th26; :: thesis: verum
end;
case p = B ; :: thesis: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p
hence (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p by A6, A26, Th26; :: thesis: verum
end;
case p = C ; :: thesis: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p
hence (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p by A6, A27, Th26; :: thesis: verum
end;
case p = E ; :: thesis: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p
hence (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p by A6, A21, Th26; :: thesis: verum
end;
case p = F ; :: thesis: (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p
hence (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p by A6, A18, Th26; :: thesis: verum
end;
end;
end;
hence (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . p in p ; :: thesis: verum
end;
Intersect FF c= xx
proof
let t be object ; :: according to TARSKI:def 3 :: thesis: ( not t in Intersect FF or t in xx )
assume A59: t in Intersect FF ; :: thesis: t in xx
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . C in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A46, ENUMSET1:def 3;
then A60: t in c by A36, A43, A59, SETFAM_1:def 1;
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . B in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A46, ENUMSET1:def 3;
then t in b by A29, A43, A59, SETFAM_1:def 1;
then A61: t in b /\ c by A60, XBOOLE_0:def 4;
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . D in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A46, ENUMSET1:def 3;
then t in d by A40, A43, A59, SETFAM_1:def 1;
then A62: t in (b /\ c) /\ d by A61, XBOOLE_0:def 4;
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . E in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A46, ENUMSET1:def 3;
then t in e by A30, A43, A59, SETFAM_1:def 1;
then A63: t in ((b /\ c) /\ d) /\ e by A62, XBOOLE_0:def 4;
(((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) . F in rng (((((B .--> b) +* (C .--> c)) +* (D .--> d)) +* (E .--> e)) +* (F .--> f)) by A46, ENUMSET1:def 3;
then t in f by A31, A43, A59, SETFAM_1:def 1;
hence t in xx by A19, A22, A25, A28, A63, XBOOLE_0:def 4; :: thesis: verum
end;
then x = Intersect FF by A47, XBOOLE_0:def 10;
hence x in '/\' (G \ {A}) by A7, A13, A12, A32, A57, A16, BVFUNC_2:def 1; :: thesis: verum
end;
A64: '/\' (G \ {A}) c= (((B '/\' C) '/\' D) '/\' E) '/\' F
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in (((B '/\' C) '/\' D) '/\' E) '/\' F )
reconsider xx = x as set by TARSKI:1;
assume x in '/\' (G \ {A}) ; :: thesis: x in (((B '/\' C) '/\' D) '/\' E) '/\' F
then consider h being Function, FF being Subset-Family of Y such that
A65: dom h = G \ {A} and
A66: rng h = FF and
A67: for d being set st d in G \ {A} holds
h . d in d and
A68: x = Intersect FF and
A69: x <> {} by BVFUNC_2:def 1;
A70: C in G \ {A} by A7, A13, A12, ENUMSET1:def 3;
then A71: h . C in C by A67;
set mbc = (h . B) /\ (h . C);
A72: B in G \ {A} by A7, A13, A12, ENUMSET1:def 3;
then h . B in B by A67;
then A73: (h . B) /\ (h . C) in INTERSECTION (B,C) by A71, SETFAM_1:def 5;
set mbcd = ((h . B) /\ (h . C)) /\ (h . D);
A74: E in G \ {A} by A7, A13, A12, ENUMSET1:def 3;
then A75: h . E in rng h by A65, FUNCT_1:def 3;
A76: h . B in rng h by A65, A72, FUNCT_1:def 3;
then A77: Intersect FF = meet (rng h) by A66, SETFAM_1:def 9;
A78: h . C in rng h by A65, A70, FUNCT_1:def 3;
A79: F in G \ {A} by A7, A13, A12, ENUMSET1:def 3;
then A80: h . F in rng h by A65, FUNCT_1:def 3;
A81: D in G \ {A} by A7, A13, A12, ENUMSET1:def 3;
then A82: h . D in rng h by A65, FUNCT_1:def 3;
A83: xx c= ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)
proof
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in xx or m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) )
assume A84: m in xx ; :: thesis: m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F)
then ( m in h . B & m in h . C ) by A68, A76, A78, A77, SETFAM_1:def 1;
then A85: m in (h . B) /\ (h . C) by XBOOLE_0:def 4;
m in h . D by A68, A82, A77, A84, SETFAM_1:def 1;
then A86: m in ((h . B) /\ (h . C)) /\ (h . D) by A85, XBOOLE_0:def 4;
m in h . E by A68, A75, A77, A84, SETFAM_1:def 1;
then A87: m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) by A86, XBOOLE_0:def 4;
m in h . F by A68, A80, A77, A84, SETFAM_1:def 1;
hence m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) by A87, XBOOLE_0:def 4; :: thesis: verum
end;
then ((h . B) /\ (h . C)) /\ (h . D) <> {} by A69;
then A88: not ((h . B) /\ (h . C)) /\ (h . D) in {{}} by TARSKI:def 1;
A89: rng h <> {} by A65, A72, FUNCT_1:3;
((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) c= xx
proof
let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) or m in xx )
assume A90: m in ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) ; :: thesis: m in xx
then A91: m in (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) by XBOOLE_0:def 4;
then A92: m in ((h . B) /\ (h . C)) /\ (h . D) by XBOOLE_0:def 4;
then A93: m in (h . B) /\ (h . C) by XBOOLE_0:def 4;
A94: rng h c= {(h . B),(h . C),(h . D),(h . E),(h . F)}
proof
let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C),(h . D),(h . E),(h . F)} )
assume u in rng h ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F)}
then consider x1 being object such that
A95: x1 in dom h and
A96: u = h . x1 by FUNCT_1:def 3;
now :: thesis: ( ( x1 = B & u in {(h . B),(h . C),(h . D),(h . E),(h . F)} ) or ( x1 = C & u in {(h . B),(h . C),(h . D),(h . E),(h . F)} ) or ( x1 = D & u in {(h . B),(h . C),(h . D),(h . E),(h . F)} ) or ( x1 = E & u in {(h . B),(h . C),(h . D),(h . E),(h . F)} ) or ( x1 = F & u in {(h . B),(h . C),(h . D),(h . E),(h . F)} ) )
per cases ( x1 = B or x1 = C or x1 = D or x1 = E or x1 = F ) by A7, A12, A65, A95, ENUMSET1:def 3;
case x1 = B ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F)}
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F)} by A96, ENUMSET1:def 3; :: thesis: verum
end;
case x1 = C ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F)}
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F)} by A96, ENUMSET1:def 3; :: thesis: verum
end;
case x1 = D ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F)}
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F)} by A96, ENUMSET1:def 3; :: thesis: verum
end;
case x1 = E ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F)}
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F)} by A96, ENUMSET1:def 3; :: thesis: verum
end;
case x1 = F ; :: thesis: u in {(h . B),(h . C),(h . D),(h . E),(h . F)}
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F)} by A96, ENUMSET1:def 3; :: thesis: verum
end;
end;
end;
hence u in {(h . B),(h . C),(h . D),(h . E),(h . F)} ; :: thesis: verum
end;
for y being set st y in rng h holds
m in y
proof
let y be set ; :: thesis: ( y in rng h implies m in y )
assume A97: y in rng h ; :: thesis: m in y
now :: thesis: ( ( y = h . B & m in y ) or ( y = h . C & m in y ) or ( y = h . D & m in y ) or ( y = h . E & m in y ) or ( y = h . F & m in y ) )
per cases ( y = h . B or y = h . C or y = h . D or y = h . E or y = h . F ) by A94, A97, ENUMSET1:def 3;
end;
end;
hence m in y ; :: thesis: verum
end;
hence m in xx by A68, A89, A77, SETFAM_1:def 1; :: thesis: verum
end;
then A98: ((((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E)) /\ (h . F) = x by A83, XBOOLE_0:def 10;
(h . B) /\ (h . C) <> {} by A69, A83;
then not (h . B) /\ (h . C) in {{}} by TARSKI:def 1;
then (h . B) /\ (h . C) in (INTERSECTION (B,C)) \ {{}} by A73, XBOOLE_0:def 5;
then A99: (h . B) /\ (h . C) in B '/\' C by PARTIT1:def 4;
h . D in D by A67, A81;
then ((h . B) /\ (h . C)) /\ (h . D) in INTERSECTION ((B '/\' C),D) by A99, SETFAM_1:def 5;
then ((h . B) /\ (h . C)) /\ (h . D) in (INTERSECTION ((B '/\' C),D)) \ {{}} by A88, XBOOLE_0:def 5;
then A100: ((h . B) /\ (h . C)) /\ (h . D) in (B '/\' C) '/\' D by PARTIT1:def 4;
set mbcde = (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E);
A101: not x in {{}} by A69, TARSKI:def 1;
(((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) <> {} by A69, A83;
then A102: not (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in {{}} by TARSKI:def 1;
h . E in E by A67, A74;
then (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in INTERSECTION (((B '/\' C) '/\' D),E) by A100, SETFAM_1:def 5;
then (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in (INTERSECTION (((B '/\' C) '/\' D),E)) \ {{}} by A102, XBOOLE_0:def 5;
then A103: (((h . B) /\ (h . C)) /\ (h . D)) /\ (h . E) in ((B '/\' C) '/\' D) '/\' E by PARTIT1:def 4;
h . F in F by A67, A79;
then x in INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F) by A98, A103, SETFAM_1:def 5;
then x in (INTERSECTION ((((B '/\' C) '/\' D) '/\' E),F)) \ {{}} by A101, XBOOLE_0:def 5;
hence x in (((B '/\' C) '/\' D) '/\' E) '/\' F by PARTIT1:def 4; :: thesis: verum
end;
CompF (A,G) = '/\' (G \ {A}) by BVFUNC_2:def 7;
hence CompF (A,G) = (((B '/\' C) '/\' D) '/\' E) '/\' F by A14, A64, XBOOLE_0:def 10; :: thesis: verum