let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B, C, D being a_partition of Y st G = {A,B,C,D} & A <> B & A <> C & A <> D holds
CompF A,G = (B '/\' C) '/\' D
let G be Subset of (PARTITIONS Y); :: thesis: for A, B, C, D being a_partition of Y st G = {A,B,C,D} & A <> B & A <> C & A <> D holds
CompF A,G = (B '/\' C) '/\' D
let A, B, C, D be a_partition of Y; :: thesis: ( G = {A,B,C,D} & A <> B & A <> C & A <> D implies CompF A,G = (B '/\' C) '/\' D )
assume that
A1: G = {A,B,C,D} and
A2: A <> B and
A3: A <> C and
A4: A <> D ; :: thesis: CompF A,G = (B '/\' C) '/\' D

per cases ( B = C or B = D or C = D or ( B <> C & B <> D & C <> D ) ) ;

suppose A5: B = C ; :: thesis: CompF A,G = (B '/\' C) '/\' D

then G = {B,B,A,D} by A1, ENUMSET1:116
.= {B,A,D} by ENUMSET1:71
.= {A,B,D} by ENUMSET1:99 ;
hence CompF A,G = B '/\' D by A2, A4, Th4
.= (B '/\' C) '/\' D by A5, PARTIT1:15 ;
:: thesis: verum

end;

suppose A6: B = D ; :: thesis: CompF A,G = (B '/\' C) '/\' D

then G = {B,B,A,C} by A1, ENUMSET1:112
.= {B,A,C} by ENUMSET1:71
.= {A,B,C} by ENUMSET1:99 ;
hence CompF A,G = B '/\' C by A2, A3, Th4
.= (B '/\' D) '/\' C by A6, PARTIT1:15
.= (B '/\' C) '/\' D by PARTIT1:16 ;
:: thesis: verum

end;

suppose A7: C = D ; :: thesis: CompF A,G = (B '/\' C) '/\' D

then G = {C,C,A,B} by A1, ENUMSET1:118
.= {C,A,B} by ENUMSET1:71
.= {A,B,C} by ENUMSET1:100 ;
hence CompF A,G = B '/\' C by A2, A3, Th4
.= B '/\' (C '/\' D) by A7, PARTIT1:15
.= (B '/\' C) '/\' D by PARTIT1:16 ;
:: thesis: verum

end;

suppose A8: ( B <> C & B <> D & C <> D ) ; :: thesis: CompF A,G = (B '/\' C) '/\' D

G \ {A} = ({A} \/ {B,C,D}) \ {A} by A1, ENUMSET1:44;
then A9: G \ {A} = ({A} \ {A}) \/ ({B,C,D} \ {A}) by XBOOLE_1:42;
A10: not B in {A} by A2, TARSKI:def 1;
A11: not C in {A} by A3, TARSKI:def 1;
A12: not D in {A} by A4, TARSKI:def 1;
{B,C,D} \ {A} = ({B} \/ {C,D}) \ {A} by ENUMSET1:42
.= ({B} \ {A}) \/ ({C,D} \ {A}) by XBOOLE_1:42
.= ({B} \ {A}) \/ {C,D} by A11, A12, ZFMISC_1:72
.= {B} \/ {C,D} by A10, ZFMISC_1:67
.= {B,C,D} by ENUMSET1:42 ;
then A13: G \ {A} = {} \/ {B,C,D} by A9, XBOOLE_1:37
.= {B,C,D} ;
A14: (B '/\' C) '/\' D c= '/\' (G \ {A})

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (B '/\' C) '/\' D or x in '/\' (G \ {A}) )
assume A15: x in (B '/\' C) '/\' D ; :: thesis: x in '/\' (G \ {A})
then x in (INTERSECTION (B '/\' C),D) \ {{} } by PARTIT1:def 4;
then consider a, d being set such that
A16: ( a in B '/\' C & d in D & x = a /\ d ) by SETFAM_1:def 5;
a in (INTERSECTION B,C) \ {{} } by A16, PARTIT1:def 4;
then consider b, c being set such that
A17: ( b in B & c in C & a = b /\ c ) by SETFAM_1:def 5;
set h = ((B .--> b) +* (C .--> c)) +* (D .--> d);
A18: dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {B,C,D} by Lm1;
A19: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D = d by FUNCT_7:96;
A20: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B = b by A8, Lm3;
A21: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C = c by A8, Lm2;
A22: for p being set st p in G \ {A} holds
(((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p

proof

let p be set ; :: thesis: ( p in G \ {A} implies (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p )
assume A23: p in G \ {A} ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p

now

per cases ( p = D or p = B or p = C ) by A13, A23, ENUMSET1:def 1;

case p = D ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p

hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p by A16, FUNCT_7:96; :: thesis: verum

end;

case p = B ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p

hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p by A8, A17, Lm3; :: thesis: verum

end;

case p = C ; :: thesis: (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p

hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p by A8, A17, Lm2; :: thesis: verum

end;

end;

end;

hence (((B .--> b) +* (C .--> c)) +* (D .--> d)) . p in p ; :: thesis: verum

end;

A24: D in dom (((B .--> b) +* (C .--> c)) +* (D .--> d)) by A18, ENUMSET1:def 1;
A25: rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) = {((((B .--> b) +* (C .--> c)) +* (D .--> d)) . B),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . C),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . D)} by Lm4
.= {((((B .--> b) +* (C .--> c)) +* (D .--> d)) . D),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . B),((((B .--> b) +* (C .--> c)) +* (D .--> d)) . C)} by ENUMSET1:100 ;
rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) c= bool Y

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) or t in bool Y )
assume A26: t in rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) ; :: thesis: t in bool Y

now

per cases ( t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D or t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B or t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C ) by A25, A26, ENUMSET1:def 1;

case t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D ; :: thesis: t in bool Y

hence t in bool Y by A16, A19; :: thesis: verum

end;

case t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B ; :: thesis: t in bool Y

hence t in bool Y by A17, A20; :: thesis: verum

end;

case t = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C ; :: thesis: t in bool Y

hence t in bool Y by A17, A21; :: thesis: verum

end;

end;

end;

hence t in bool Y ; :: thesis: verum

end;

then reconsider F = rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) as Subset-Family of Y ;
A27: rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) <> {} by A24, FUNCT_1:12;
A28: x c= Intersect F

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in x or u in Intersect F )
assume A29: u in x ; :: thesis: u in Intersect F
for y being set st y in F holds
u in y

proof

let y be set ; :: thesis: ( y in F implies u in y )
assume A30: y in F ; :: thesis: u in y

now

per cases ( y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D or y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B or y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C ) by A25, A30, ENUMSET1:def 1;

case y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D ; :: thesis: u in y

hence u in y by A16, A19, A29, XBOOLE_0:def 4; :: thesis: verum

end;

case A31: y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B ; :: thesis: u in y

u in b /\ (c /\ d) by A16, A17, A29, XBOOLE_1:16;
hence u in y by A20, A31, XBOOLE_0:def 4; :: thesis: verum

end;

case A32: y = (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C ; :: thesis: u in y

u in c /\ (b /\ d) by A16, A17, A29, XBOOLE_1:16;
hence u in y by A21, A32, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence u in y ; :: thesis: verum

end;

then u in meet F by A25, SETFAM_1:def 1;
hence u in Intersect F by A25, SETFAM_1:def 10; :: thesis: verum

end;

Intersect F c= x

proof

let t be set ; :: according to TARSKI:def 3 :: thesis: ( not t in Intersect F or t in x )
assume t in Intersect F ; :: thesis: t in x
then A33: t in meet (rng (((B .--> b) +* (C .--> c)) +* (D .--> d))) by A27, SETFAM_1:def 10;
( (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B in rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) & (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C in rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) & (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D in rng (((B .--> b) +* (C .--> c)) +* (D .--> d)) ) by A25, ENUMSET1:def 1;
then A34: ( t in (((B .--> b) +* (C .--> c)) +* (D .--> d)) . B & t in (((B .--> b) +* (C .--> c)) +* (D .--> d)) . C & t in (((B .--> b) +* (C .--> c)) +* (D .--> d)) . D ) by A33, SETFAM_1:def 1;
then t in b /\ c by A20, A21, XBOOLE_0:def 4;
hence t in x by A16, A17, A19, A34, XBOOLE_0:def 4; :: thesis: verum

end;

then A35: x = Intersect F by A28, XBOOLE_0:def 10;
x <> {} by A15, EQREL_1:def 6;
hence x in '/\' (G \ {A}) by A13, A18, A22, A35, BVFUNC_2:def 1; :: thesis: verum

end;

'/\' (G \ {A}) c= (B '/\' C) '/\' D

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' (G \ {A}) or x in (B '/\' C) '/\' D )
assume x in '/\' (G \ {A}) ; :: thesis: x in (B '/\' C) '/\' D
then consider h being Function, F being Subset-Family of Y such that
A36: ( dom h = G \ {A} & rng h = F & ( for d being set st d in G \ {A} holds
h . d in d ) & x = Intersect F & x <> {} ) by BVFUNC_2:def 1;
( B in G \ {A} & C in G \ {A} & D in G \ {A} ) by A13, ENUMSET1:def 1;
then A37: ( h . B in B & h . C in C & h . D in D ) by A36;
( B in dom h & C in dom h & D in dom h ) by A13, A36, ENUMSET1:def 1;
then A38: ( h . B in rng h & h . C in rng h & h . D in rng h ) by FUNCT_1:def 5;
A39: not x in {{} } by A36, TARSKI:def 1;
A40: ((h . B) /\ (h . C)) /\ (h . D) c= x

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in ((h . B) /\ (h . C)) /\ (h . D) or m in x )
assume A41: m in ((h . B) /\ (h . C)) /\ (h . D) ; :: thesis: m in x
then A42: ( m in (h . B) /\ (h . C) & m in h . D ) by XBOOLE_0:def 4;
A43: rng h c= {(h . B),(h . C),(h . D)}

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . B),(h . C),(h . D)} )
assume u in rng h ; :: thesis: u in {(h . B),(h . C),(h . D)}
then consider x1 being set such that
A44: ( x1 in dom h & u = h . x1 ) by FUNCT_1:def 5;

now

per cases ( x1 = B or x1 = C or x1 = D ) by A13, A36, A44, ENUMSET1:def 1;

case x1 = B ; :: thesis: u in {(h . B),(h . C),(h . D)}

hence u in {(h . B),(h . C),(h . D)} by A44, ENUMSET1:def 1; :: thesis: verum

end;

case x1 = C ; :: thesis: u in {(h . B),(h . C),(h . D)}

hence u in {(h . B),(h . C),(h . D)} by A44, ENUMSET1:def 1; :: thesis: verum

end;

case x1 = D ; :: thesis: u in {(h . B),(h . C),(h . D)}

hence u in {(h . B),(h . C),(h . D)} by A44, ENUMSET1:def 1; :: thesis: verum

end;

end;

end;

hence u in {(h . B),(h . C),(h . D)} ; :: 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 A45: y in rng h ; :: thesis: m in y

now

per cases ( y = h . B or y = h . C or y = h . D ) by A43, A45, ENUMSET1:def 1;

case y = h . B ; :: thesis: m in y

hence m in y by A42, XBOOLE_0:def 4; :: thesis: verum

end;

case y = h . C ; :: thesis: m in y

hence m in y by A42, XBOOLE_0:def 4; :: thesis: verum

end;

case y = h . D ; :: thesis: m in y

hence m in y by A41, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence m in y ; :: thesis: verum

end;

then m in meet (rng h) by A38, SETFAM_1:def 1;
hence m in x by A36, A38, SETFAM_1:def 10; :: thesis: verum

end;

A46: x c= ((h . B) /\ (h . C)) /\ (h . D)

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in x or m in ((h . B) /\ (h . C)) /\ (h . D) )
assume m in x ; :: thesis: m in ((h . B) /\ (h . C)) /\ (h . D)
then m in meet (rng h) by A36, A38, SETFAM_1:def 10;
then A47: ( m in h . B & m in h . C & m in h . D ) by A38, SETFAM_1:def 1;
then m in (h . B) /\ (h . C) by XBOOLE_0:def 4;
hence m in ((h . B) /\ (h . C)) /\ (h . D) by A47, XBOOLE_0:def 4; :: thesis: verum

end;

then A48: ((h . B) /\ (h . C)) /\ (h . D) = x by A40, XBOOLE_0:def 10;
set m = (h . B) /\ (h . C);
(h . B) /\ (h . C) <> {} by A36, A46;
then A49: not (h . B) /\ (h . C) in {{} } by TARSKI:def 1;
(h . B) /\ (h . C) in INTERSECTION B,C by A37, SETFAM_1:def 5;
then (h . B) /\ (h . C) in (INTERSECTION B,C) \ {{} } by A49, XBOOLE_0:def 5;
then (h . B) /\ (h . C) in B '/\' C by PARTIT1:def 4;
then x in INTERSECTION (B '/\' C),D by A37, A48, SETFAM_1:def 5;
then x in (INTERSECTION (B '/\' C),D) \ {{} } by A39, XBOOLE_0:def 5;
hence x in (B '/\' C) '/\' D by PARTIT1:def 4; :: thesis: verum

end;

then '/\' (G \ {A}) = (B '/\' C) '/\' D by A14, XBOOLE_0:def 10;
hence CompF A,G = (B '/\' C) '/\' D by BVFUNC_2:def 7; :: thesis: verum

end;

end;