let X be set ; :: thesis: for a, b being Element of DISJOINT_PAIRS X st not a \/ b in DISJOINT_PAIRS X holds
ex p being Element of X st
( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )
let a, b be Element of DISJOINT_PAIRS X; :: thesis: ( not a \/ b in DISJOINT_PAIRS X implies ex p being Element of X st
( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) )
set p = the Element of ((a \/ b) `1) /\ ((a \/ b) `2);
assume not a \/ b in DISJOINT_PAIRS X ; :: thesis: ex p being Element of X st
( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )
then (a \/ b) `1 meets (a \/ b) `2 ;
then A1: ((a \/ b) `1) /\ ((a \/ b) `2) <> {} ;
((a \/ b) `1) /\ ((a \/ b) `2) is Subset of X by FINSUB_1:16;
then reconsider p = the Element of ((a \/ b) `1) /\ ((a \/ b) `2) as Element of X by A1, TARSKI:def 3;
p in (a \/ b) `2 by A1, XBOOLE_0:def 4;
then p in (a `2) \/ (b `2) ;
then A2: ( p in b `2 or p in a `2 ) by XBOOLE_0:def 3;
take p ; :: thesis: ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) )
p in (a \/ b) `1 by A1, XBOOLE_0:def 4;
then p in (a `1) \/ (b `1) ;
then ( p in a `1 or p in b `1 ) by XBOOLE_0:def 3;
hence ( ( p in a `1 & p in b `2 ) or ( p in b `1 & p in a `2 ) ) by A2, Th27; :: thesis: verum