let Y be non empty set ; :: thesis: for G being Subset of (PARTITIONS Y)
for A, B being a_partition of Y st G is independent & 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 is independent & G = {A,B} & A <> B holds
'/\' G = A '/\' B
let A, B be a_partition of Y; :: thesis: ( G is independent & G = {A,B} & A <> B implies '/\' G = A '/\' B )
assume that
A1: G is independent and
A2: G = {A,B} and
A3: A <> B ; :: thesis: '/\' G = A '/\' B
A4: '/\' 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
A5: dom h = G and
A6: rng h = F and
A7: for d being set st d in G holds
h . d in d and
A8: x = Intersect F and
A9: x <> {} by BVFUNC_2:def 1;
A10: not x in {{}} by A9, TARSKI:def 1;
A11: A in G by A2, TARSKI:def 2;
then A12: h . A in rng h by A5, FUNCT_1:def 3;
then A13: Intersect F = meet (rng h) by A6, SETFAM_1:def 9;
A14: (h . A) /\ (h . B) c= xx

proof

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

proof

thus rng h c= {(h . A),(h . B)} :: according to XBOOLE_0:def 10 :: thesis: {(h . A),(h . B)} c= rng h

proof

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in rng h or m in {(h . A),(h . B)} )
assume m in rng h ; :: thesis: m in {(h . A),(h . B)}
then consider w being object such that
A16: w in dom h and
A17: m = h . w by FUNCT_1:def 3;
( w = A or w = B ) by A2, A5, A16, TARSKI:def 2;
hence m in {(h . A),(h . B)} by A17, TARSKI:def 2; :: thesis: verum

end;

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in {(h . A),(h . B)} or m in rng h )
assume m in {(h . A),(h . B)} ; :: thesis: m in rng h
then A18: ( m = h . A or m = h . B ) by TARSKI:def 2;
A19: B in dom h by A2, A5, TARSKI:def 2;
A in dom h by A2, A5, TARSKI:def 2;
hence m in rng h by A18, A19, FUNCT_1:def 3; :: thesis: verum

end;

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in (h . A) /\ (h . B) or m in xx )
assume A20: m in (h . A) /\ (h . B) ; :: thesis: m in xx
then A21: m in h . B by XBOOLE_0:def 4;
m in h . A by A20, XBOOLE_0:def 4;
then for y being set st y in rng h holds
m in y by A21, A15, TARSKI:def 2;
hence m in xx by A8, A12, A13, SETFAM_1:def 1; :: thesis: verum

end;

A22: B in G by A2, TARSKI:def 2;
then A23: h . B in B by A7;
A24: h . B in rng h by A5, A22, 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 A25: m in xx ; :: thesis: m in (h . A) /\ (h . B)
then A26: m in h . B by A8, A24, A13, SETFAM_1:def 1;
m in h . A by A8, A12, A13, A25, SETFAM_1:def 1;
hence m in (h . A) /\ (h . B) by A26, XBOOLE_0:def 4; :: thesis: verum

end;

then A27: (h . A) /\ (h . B) = x by A14, XBOOLE_0:def 10;
h . A in A by A7, A11;
then x in INTERSECTION (A,B) by A23, A27, SETFAM_1:def 5;
then x in (INTERSECTION (A,B)) \ {{}} by A10, XBOOLE_0:def 5;
hence x in A '/\' B by PARTIT1:def 4; :: thesis: verum

end;

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

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A '/\' B or x in '/\' G )
assume x in A '/\' B ; :: thesis: x in '/\' G
then x in (INTERSECTION (A,B)) \ {{}} by PARTIT1:def 4;
then consider X, Z being set such that
A28: X in A and
A29: Z in B and
A30: x = X /\ Z by SETFAM_1:def 5;
{X,Z} c= bool Y

proof

let m be object ; :: according to TARSKI:def 3 :: thesis: ( not m in {X,Z} or m in bool Y )
assume m in {X,Z} ; :: thesis: m in bool Y
then ( m = X or m = Z ) by TARSKI:def 2;
hence m in bool Y by A28, A29; :: thesis: verum

end;

then reconsider SS = {X,Z} as Subset-Family of Y ;
A31: X /\ Z = Intersect SS by A28, A29, MSSUBFAM:10;
set h = (A,B) --> (X,Z);
A32: for d being set st d in G holds
((A,B) --> (X,Z)) . d in d

proof

let d be set ; :: thesis: ( d in G implies ((A,B) --> (X,Z)) . d in d )
assume d in G ; :: thesis: ((A,B) --> (X,Z)) . d in d
then ( d = A or d = B ) by A2, TARSKI:def 2;
hence ((A,B) --> (X,Z)) . d in d by A3, A28, A29, FUNCT_4:63; :: thesis: verum

end;

A33: dom ((A,B) --> (X,Z)) = {A,B} by FUNCT_4:62;
A34: rng ((A,B) --> (X,Z)) = SS by A3, FUNCT_4:64;
then Intersect SS <> {} by A1, A2, A33, A32, BVFUNC_2:def 5;
hence x in '/\' G by A2, A30, A33, A34, A32, A31, BVFUNC_2:def 1; :: thesis: verum

end;

hence '/\' G = A '/\' B by A4; :: thesis: verum