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 A1: ( G = {A,B} & A <> B ) ; :: thesis: '/\' G = A '/\' B
A2: A '/\' B c= '/\' G

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A '/\' B or x in '/\' G )
assume A3: x in A '/\' B ; :: thesis: x in '/\' G
then x in (INTERSECTION A,B) \ {{} } by PARTIT1:def 4;
then consider a, b being set such that
A4: ( a in A & b in B & x = a /\ b ) by SETFAM_1:def 5;
set h0 = A,B --> a,b;
A5: dom (A,B --> a,b) = {A,B} by FUNCT_4:65;
A6: rng (A,B --> a,b) = {a,b} by A1, FUNCT_4:67;
A7: rng (A,B --> a,b) = {a,b} by A1, FUNCT_4:67;
rng (A,B --> a,b) c= bool Y

proof

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

now

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

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

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

end;

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

hence y in bool Y by A4; :: 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 ;
A9: 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 A10: d in G ; :: thesis: (A,B --> a,b) . d in d

now

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

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

hence (A,B --> a,b) . d in d by A1, A4, FUNCT_4:66; :: thesis: verum

end;

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

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

end;

end;

end;

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

end;

A11: 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 A12: 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 A13: y in F ; :: thesis: u in y

now

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

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

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

end;

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

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

end;

end;

end;

hence u in y ; :: thesis: verum

end;

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

end;

Intersect F c= x

proof

let u be set ; :: according to TARSKI:def 3 :: thesis: ( not u in Intersect F or u in x )
assume A14: u in Intersect F ; :: thesis: u in x
A15: ( a in {a,b} & b in {a,b} ) by TARSKI:def 2;
then ( a in F & b in F ) by A1, FUNCT_4:67;
then Intersect F = meet F by SETFAM_1:def 10;
then ( u in a & u in b ) by A7, A14, A15, SETFAM_1:def 1;
hence u in x by A4, XBOOLE_0:def 4; :: thesis: verum

end;

then A16: x = Intersect F by A11, XBOOLE_0:def 10;
x <> {} by A3, EQREL_1:def 6;
hence x in '/\' G by A1, A5, A9, A16, BVFUNC_2:def 1; :: thesis: verum

end;

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in '/\' G or x in A '/\' B )
assume x in '/\' G ; :: thesis: x in A '/\' B
then consider h being Function, F being Subset-Family of Y such that
A17: ( dom h = G & rng h = F & ( for d being set st d in G holds
h . d in d ) & x = Intersect F & x <> {} ) by BVFUNC_2:def 1;
( A in G & B in G ) by A1, TARSKI:def 2;
then A18: ( h . A in A & h . B in B ) by A17;
( A in dom h & B in dom h ) by A1, A17, TARSKI:def 2;
then A19: ( h . A in rng h & h . B in rng h ) by FUNCT_1:def 5;
A20: not x in {{} } by A17, TARSKI:def 1;
A21: (h . A) /\ (h . B) c= x

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in (h . A) /\ (h . B) or m in x )
assume A22: m in (h . A) /\ (h . B) ; :: thesis: m in x
A23: rng h c= {(h . A),(h . B)}

proof

let u be set ; :: 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 set such that
A24: ( x1 in dom h & u = h . x1 ) by FUNCT_1:def 5;

now

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

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

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

end;

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

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

now

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

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

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

end;

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

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

end;

end;

end;

hence m in y ; :: thesis: verum

end;

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

end;

x c= (h . A) /\ (h . B)

proof

let m be set ; :: according to TARSKI:def 3 :: thesis: ( not m in x or m in (h . A) /\ (h . B) )
assume m in x ; :: thesis: m in (h . A) /\ (h . B)
then m in meet (rng h) by A17, A19, SETFAM_1:def 10;
then ( m in h . A & m in h . B ) by A19, 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 A21, XBOOLE_0:def 10;
then x in INTERSECTION A,B by A18, SETFAM_1:def 5;
then x in (INTERSECTION A,B) \ {{} } by A20, XBOOLE_0:def 5;
hence x in A '/\' B by PARTIT1:def 4; :: thesis: verum

end;

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