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

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