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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A '/\' B or x in '/\' G )
reconsider xx = x as set by TARSKI:1;
assume A4: x in A '/\' B ; :: thesis: x in '/\' G
then A5: x <> {} by EQREL_1:def 4;
x in (INTERSECTION (A,B)) \ {{}} by A4, PARTIT1:def 4;
then consider a, b being set such that
A6: a in A and
A7: b in B and
A8: x = a /\ b by SETFAM_1:def 5;
set h0 = (A,B) --> (a,b);
A9: rng ((A,B) --> (a,b)) = {a,b} by A2, FUNCT_4:64;
rng ((A,B) --> (a,b)) c= bool Y

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((A,B) --> (a,b)) or y in bool Y )
assume A10: y in rng ((A,B) --> (a,b)) ; :: thesis: y in bool Y

now :: thesis: ( ( y = a & y in bool Y ) or ( y = b & y in bool Y ) )

per cases ( y = a or y = b ) by A9, A10, TARSKI:def 2;

case y = a ; :: thesis: y in bool Y

hence y in bool Y by A6; :: thesis: verum

end;

case y = b ; :: thesis: y in bool Y

hence y in bool Y by A7; :: thesis: verum

end;

end;

end;

hence y in bool Y ; :: thesis: verum

end;

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

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in xx or u in Intersect F )
assume A12: u in xx ; :: 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 A13: y in F ; :: thesis: u in y

now :: thesis: ( ( y = a & u in y ) or ( y = b & u in y ) )

per cases ( y = a or y = b ) by A9, A13, TARSKI:def 2;

case y = a ; :: thesis: u in y

hence u in y by A8, A12, XBOOLE_0:def 4; :: thesis: verum

end;

case y = b ; :: thesis: u in y

hence u in y by A8, A12, XBOOLE_0:def 4; :: thesis: verum

end;

end;

end;

hence u in y ; :: thesis: verum

end;

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

end;

A14: for d being set st d in G holds
((A,B) --> (a,b)) . d in d

proof

let d be set ; :: thesis: ( d in G implies ((A,B) --> (a,b)) . d in d )
assume A15: d in G ; :: thesis: ((A,B) --> (a,b)) . d in d

now :: thesis: ( ( d = A & ((A,B) --> (a,b)) . d in d ) or ( d = B & ((A,B) --> (a,b)) . d in d ) )

per cases ( d = A or d = B ) by A1, A15, TARSKI:def 2;

case d = A ; :: thesis: ((A,B) --> (a,b)) . d in d

hence ((A,B) --> (a,b)) . d in d by A2, A6, FUNCT_4:63; :: thesis: verum

end;

case d = B ; :: thesis: ((A,B) --> (a,b)) . d in d

hence ((A,B) --> (a,b)) . d in d by A7, FUNCT_4:63; :: thesis: verum

end;

end;

end;

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

end;

A16: rng ((A,B) --> (a,b)) = {a,b} by A2, FUNCT_4:64;
Intersect F c= xx

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in Intersect F or u in xx )
assume A17: u in Intersect F ; :: thesis: u in xx
A18: a in {a,b} by TARSKI:def 2;
then a in F by A2, FUNCT_4:64;
then A19: Intersect F = meet F by SETFAM_1:def 9;
b in {a,b} by TARSKI:def 2;
then A20: u in b by A16, A17, A19, SETFAM_1:def 1;
u in a by A16, A17, A18, A19, SETFAM_1:def 1;
hence u in xx by A8, A20, XBOOLE_0:def 4; :: thesis: verum

end;

then ( dom ((A,B) --> (a,b)) = {A,B} & x = Intersect F ) by A11, FUNCT_4:62, XBOOLE_0:def 10;
hence x in '/\' G by A1, A14, A5, BVFUNC_2:def 1; :: thesis: verum

end;

'/\' G c= A '/\' B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' G or x in A '/\' B )
reconsider xx = x as set by TARSKI:1;
assume x in '/\' G ; :: thesis: x in A '/\' B
then consider h being Function, F being Subset-Family of Y such that
A21: dom h = G and
A22: rng h = F and
A23: for d being set st d in G holds
h . d in d and
A24: x = Intersect F and
A25: x <> {} by BVFUNC_2:def 1;
A26: not x in {{}} by A25, TARSKI:def 1;
A in dom h by A1, A21, TARSKI:def 2;
then A27: h . A in rng h by FUNCT_1:def 3;
A28: (h . A) /\ (h . B) c= xx

proof

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in (h . A) /\ (h . B) or m in xx )
assume A29: m in (h . A) /\ (h . B) ; :: thesis: m in xx
A30: rng h c= {(h . A),(h . B)}

proof

let u be object ; :: according to TARSKI:def 3 :: thesis: ( not u in rng h or u in {(h . A),(h . B)} )
assume u in rng h ; :: thesis: u in {(h . A),(h . B)}
then consider x1 being object such that
A31: x1 in dom h and
A32: u = h . x1 by FUNCT_1:def 3;

now :: thesis: ( ( x1 = A & u in {(h . A),(h . B)} ) or ( x1 = B & u in {(h . A),(h . B)} ) )

per cases ( x1 = A or x1 = B ) by A1, A21, A31, TARSKI:def 2;

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

hence u in {(h . A),(h . B)} by A32, TARSKI:def 2; :: thesis: verum

end;

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

hence u in {(h . A),(h . B)} by A32, TARSKI:def 2; :: thesis: verum

end;

end;

end;

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

now :: thesis: ( ( y = h . A & m in y ) or ( y = h . B & m in y ) )

per cases ( y = h . A or y = h . B ) by A30, A33, TARSKI:def 2;

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

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

end;

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

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

end;

end;

end;

hence m in y ; :: thesis: verum

end;

then m in meet (rng h) by A27, SETFAM_1:def 1;
hence m in xx by A22, A24, A27, SETFAM_1:def 9; :: thesis: verum

end;

B in G by A1, TARSKI:def 2;
then A34: h . B in B by A23;
A in G by A1, TARSKI:def 2;
then A35: h . A in A by A23;
B in dom h by A1, A21, TARSKI:def 2;
then A36: h . B in rng h by FUNCT_1:def 3;
xx c= (h . A) /\ (h . B)

proof

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in xx or m in (h . A) /\ (h . B) )
assume m in xx ; :: thesis: m in (h . A) /\ (h . B)
then m in meet (rng h) by A22, A24, A27, SETFAM_1:def 9;
then ( m in h . A & m in h . B ) by A27, A36, SETFAM_1:def 1;
hence m in (h . A) /\ (h . B) by XBOOLE_0:def 4; :: thesis: verum

end;

then (h . A) /\ (h . B) = x by A28, XBOOLE_0:def 10;
then x in INTERSECTION (A,B) by A35, A34, SETFAM_1:def 5;
then x in (INTERSECTION (A,B)) \ {{}} by A26, XBOOLE_0:def 5;
hence x in A '/\' B by PARTIT1:def 4; :: thesis: verum

end;

hence '/\' G = A '/\' B by A3, XBOOLE_0:def 10; :: thesis: verum