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
for a, b being set st a in A & b in B holds
a meets 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
for a, b being set st a in A & b in B holds
a meets b
let A, B be a_partition of Y; :: thesis: ( G is independent & G = {A,B} & A <> B implies for a, b being set st a in A & b in B holds
a meets b )
assume that
A1: G is independent and
A2: G = {A,B} and
A3: A <> B ; :: thesis: for a, b being set st a in A & b in B holds
a meets b
let a, b be set ; :: thesis: ( a in A & b in B implies a meets b )
assume that
A4: a in A and
A5: b in B ; :: thesis: a meets b
set h2 = A,B --> a,b;
A6: 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 d in G ; :: thesis: (A,B --> a,b) . d in d
then ( d = A or d = B ) by A2, TARSKI:def 2;
hence (A,B --> a,b) . d in d by A3, A4, A5, FUNCT_4:66; :: thesis: verum

end;

{a,b} c= bool Y

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {a,b} or x in bool Y )
assume x in {a,b} ; :: thesis: x in bool Y
then ( x = a or x = b ) by TARSKI:def 2;
hence x in bool Y by A4, A5; :: thesis: verum

end;

then reconsider SS = {a,b} as Subset-Family of Y ;
A7: dom (A,B --> a,b) = {A,B} by FUNCT_4:65;
rng (A,B --> a,b) = SS by A3, FUNCT_4:67;
then Intersect SS <> {} by A1, A2, A7, A6, BVFUNC_2:def 5;
hence a /\ b <> {} by A4, A5, MSSUBFAM:10; :: according to XBOOLE_0:def 7 :: thesis: verum