let Y be non empty set ; :: thesis:
let G be Subset of (PARTITIONS Y); :: thesis:
let A, B, C be a_partition of Y; :: thesis:
assume that
A1: G = {A,B,C} and
A2: A <> B and
A3: C <> A ; :: thesis:

per cases ;

suppose A4: B = C ; :: thesis:

G = {B,C,A} by A1, ENUMSET1:59
.= {B,A} by A4, ENUMSET1:30 ;
hence CompF (A,G) = B by A2, BVFUNC11:7
.= B '/\' C by A4, PARTIT1:13 ;
:: thesis:

end;

suppose A5: B <> C ; :: thesis:

A6: G \ {A} = ({A} \/ {B,C}) \ {A} by A1, ENUMSET1:2
.= ({A} \ {A}) \/ ({B,C} \ {A}) by XBOOLE_1:42 ;
( not B in {A} & not C in {A} ) by A2, A3, TARSKI:def 1;
then A7: G \ {A} = ({A} \ {A}) \/ {B,C} by A6, ZFMISC_1:63
.= {} \/ {B,C} by XBOOLE_1:37
.= {B,C} ;
A8: '/\' (G \ {A}) c= B '/\' C

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
assume x in '/\' (G \ {A}) ; :: thesis:
then consider h being Function, F being Subset-Family of Y such that
A9: dom h = G \ {A} and
A10: rng h = F and
A11: for d being set st d in G \ {A} holds
h . d in d and
A12: x = Intersect F and
A13: x <> {} by BVFUNC_2:def 1;
A14: not x in {{}} by A13, TARSKI:def 1;
B in dom h by A7, A9, TARSKI:def 2;
then A15: h . B in rng h by FUNCT_1:def 3;
A16: (h . B) /\ (h . C) c= xx

proof

let m be object ; :: according to TARSKI:def 3 :: thesis:
assume A17: m in (h . B) /\ (h . C) ; :: thesis:
A18: rng h c= {(h . B),(h . C)}

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume u in rng h ; :: thesis:
then consider x1 being object such that
A19: x1 in dom h and
A20: u = h . x1 by FUNCT_1:def 3;

now :: thesis:

per cases by A7, A9, A19, TARSKI:def 2;

case x1 = B ; :: thesis:

hence u in {(h . B),(h . C)} by A20, TARSKI:def 2; :: thesis:

end;

case x1 = C ; :: thesis:

hence u in {(h . B),(h . C)} by A20, TARSKI:def 2; :: thesis:

end;

end;

end;

hence u in {(h . B),(h . C)} ; :: thesis:

end;

for y being set st y in rng h holds
m in y

proof

let y be set ; :: thesis:
assume A21: y in rng h ; :: thesis:

now :: thesis:

per cases by A18, A21, TARSKI:def 2;

case y = h . B ; :: thesis:

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

end;

case y = h . C ; :: thesis:

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

end;

end;

end;

hence m in y ; :: thesis:

end;

then m in meet (rng h) by A15, SETFAM_1:def 1;
hence m in xx by A10, A12, A15, SETFAM_1:def 9; :: thesis:

end;

C in G \ {A} by A7, TARSKI:def 2;
then A22: h . C in C by A11;
B in G \ {A} by A7, TARSKI:def 2;
then A23: h . B in B by A11;
C in dom h by A7, A9, TARSKI:def 2;
then A24: h . C in rng h by FUNCT_1:def 3;
xx c= (h . B) /\ (h . C)

proof

let m be object ; :: according to TARSKI:def 3 :: thesis:
assume m in xx ; :: thesis:
then m in meet (rng h) by A10, A12, A15, SETFAM_1:def 9;
then ( m in h . B & m in h . C ) by A15, A24, SETFAM_1:def 1;
hence m in (h . B) /\ (h . C) by XBOOLE_0:def 4; :: thesis:

end;

then (h . B) /\ (h . C) = x by A16, XBOOLE_0:def 10;
then x in INTERSECTION (B,C) by A23, A22, SETFAM_1:def 5;
then x in (INTERSECTION (B,C)) \ {{}} by A14, XBOOLE_0:def 5;
hence x in B '/\' C by PARTIT1:def 4; :: thesis:

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
reconsider xx = x as set by TARSKI:1;
assume A26: x in B '/\' C ; :: thesis:
then A27: x <> {} by EQREL_1:def 4;
x in (INTERSECTION (B,C)) \ {{}} by A26, PARTIT1:def 4;
then consider a, b being set such that
A28: a in B and
A29: b in C and
A30: x = a /\ b by SETFAM_1:def 5;
set h0 = (B,C) --> (a,b);
A31: dom ((B,C) --> (a,b)) = G \ {A} by A7, FUNCT_4:62;
A32: rng ((B,C) --> (a,b)) = {a,b} by A5, FUNCT_4:64;
rng ((B,C) --> (a,b)) c= bool Y

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume A33: y in rng ((B,C) --> (a,b)) ; :: thesis:

now :: thesis:

per cases by A32, A33, TARSKI:def 2;

case y = a ; :: thesis:

hence y in bool Y by A28; :: thesis:

end;

case y = b ; :: thesis:

hence y in bool Y by A29; :: thesis:

end;

end;

end;

hence y in bool Y ; :: thesis:

end;

then reconsider F = rng ((B,C) --> (a,b)) as Subset-Family of Y ;
A34: xx c= Intersect F

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume A35: u in xx ; :: thesis:
for y being set st y in F holds
u in y

proof

let y be set ; :: thesis:
assume A36: y in F ; :: thesis:

now :: thesis:

per cases by A32, A36, TARSKI:def 2;

case y = a ; :: thesis:

hence u in y by A30, A35, XBOOLE_0:def 4; :: thesis:

end;

case y = b ; :: thesis:

hence u in y by A30, A35, XBOOLE_0:def 4; :: thesis:

end;

end;

end;

hence u in y ; :: thesis:

end;

then u in meet F by A32, SETFAM_1:def 1;
hence u in Intersect F by A32, SETFAM_1:def 9; :: thesis:

end;

A37: for d being set st d in G \ {A} holds
((B,C) --> (a,b)) . d in d

proof

let d be set ; :: thesis:
assume A38: d in G \ {A} ; :: thesis:

now :: thesis:

per cases by A7, A38, TARSKI:def 2;

case d = B ; :: thesis:

hence ((B,C) --> (a,b)) . d in d by A5, A28, FUNCT_4:63; :: thesis:

end;

case d = C ; :: thesis:

hence ((B,C) --> (a,b)) . d in d by A29, FUNCT_4:63; :: thesis:

end;

end;

end;

hence ((B,C) --> (a,b)) . d in d ; :: thesis:

end;

Intersect F c= xx

proof

let u be object ; :: according to TARSKI:def 3 :: thesis:
assume A39: u in Intersect F ; :: thesis:
A40: Intersect F = meet F by A32, SETFAM_1:def 9;
b in F by A32, TARSKI:def 2;
then A41: u in b by A39, A40, SETFAM_1:def 1;
a in F by A32, TARSKI:def 2;
then u in a by A39, A40, SETFAM_1:def 1;
hence u in xx by A30, A41, XBOOLE_0:def 4; :: thesis:

end;

then x = Intersect F by A34, XBOOLE_0:def 10;
hence x in '/\' (G \ {A}) by A31, A37, A27, BVFUNC_2:def 1; :: thesis:

end;

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

end;

end;