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} & 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 A3: ( a in A & b in B ) ; :: thesis: a meets b
set h2 = A,B --> a,b;
{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 A3; :: thesis: verum

end;

then reconsider SS = {a,b} as Subset-Family of Y ;
A4: ( dom (A,B --> a,b) = {A,B} & rng (A,B --> a,b) = SS ) by A2, FUNCT_4:65, FUNCT_4:67;
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 A2, A3, FUNCT_4:66; :: thesis: verum

end;

then Intersect SS <> {} by A1, A2, A4, BVFUNC_2:def 5;
hence a /\ b <> {} by A3, MSSUBFAM:10; :: according to XBOOLE_0:def 7 :: thesis: verum