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 ;
p in (a \/ b) `2 by ;
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 ;
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 ; :: thesis: verum