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

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

'/\' G c= A '/\' B
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

A11: xx c= Intersect F

((A,B) --> (a,b)) . d in d

Intersect F c= xx

hence x in '/\' G by A1, A14, A5, BVFUNC_2:def 1; :: thesis: verum

end;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

then reconsider F = rng ((A,B) --> (a,b)) as Subset-Family of Y ;
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

hence y in bool Y ; :: thesis: verum

end;assume A10: y in rng ((A,B) --> (a,b)) ; :: thesis: y in bool Y

hence y in bool Y ; :: thesis: verum

A11: xx c= Intersect F

proof

A14:
for d being set st d in G holds
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

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

end;assume A12: u in xx ; :: thesis: u in Intersect F

for y being set st y in F holds

u in y

proof

then
u in meet F
by A9, SETFAM_1:def 1;
let y be set ; :: thesis: ( y in F implies u in y )

assume A13: y in F ; :: thesis: u in y

end;assume A13: y in F ; :: thesis: u in y

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

hence
u in y
; :: thesis: verumhence u in Intersect F by A9, SETFAM_1:def 9; :: thesis: verum

((A,B) --> (a,b)) . d in d

proof

A16:
rng ((A,B) --> (a,b)) = {a,b}
by A2, FUNCT_4:64;
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

end;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 ) )

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

Intersect F c= xx

proof

then
( dom ((A,B) --> (a,b)) = {A,B} & x = Intersect F )
by A11, FUNCT_4:62, XBOOLE_0:def 10;
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;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

hence x in '/\' G by A1, A14, A5, BVFUNC_2:def 1; :: thesis: verum

proof

hence
'/\' G = A '/\' B
by A3, XBOOLE_0:def 10; :: thesis: verum
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

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)

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;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

B in G
by A1, TARSKI:def 2;
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)}

m in y

hence m in xx by A22, A24, A27, SETFAM_1:def 9; :: thesis: verum

end;assume A29: m in (h . A) /\ (h . B) ; :: thesis: m in xx

A30: rng h c= {(h . A),(h . B)}

proof

for y being set st y in rng h holds
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;

end;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)} ) )

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

m in y

proof

then
m in meet (rng h)
by A27, SETFAM_1:def 1;
let y be set ; :: thesis: ( y in rng h implies m in y )

assume A33: y in rng h ; :: thesis: m in y

end;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 ) )end;

hence
m in y
; :: thesis: verumhence m in xx by A22, A24, A27, SETFAM_1:def 9; :: thesis: verum

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

then
(h . A) /\ (h . B) = x
by A28, XBOOLE_0:def 10;
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;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

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