let X be set ; :: thesis: for y, x being Element of [:(Fin X),(Fin X):] st y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X holds
( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )
let y, x be Element of [:(Fin X),(Fin X):]; :: thesis: ( y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X implies ( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ) )
assume that
A1: y in DISJOINT_PAIRS X and
A2: x in DISJOINT_PAIRS X ; :: thesis: ( y \/ x in DISJOINT_PAIRS X iff ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} )
A3: ( ((y `1) \/ (x `1)) /\ ((y `2) \/ (x `2)) = (((y `1) \/ (x `1)) /\ (y `2)) \/ (((y `1) \/ (x `1)) /\ (x `2)) & ((y `1) \/ (x `1)) /\ (y `2) = ((y `1) /\ (y `2)) \/ ((x `1) /\ (y `2)) ) by XBOOLE_1:23;
x `1 misses x `2 by A2, Th42;
then A4: (x `1) /\ (x `2) = {} by XBOOLE_0:def 7;
y `1 misses y `2 by A1, Th42;
then A5: (y `1) /\ (y `2) = {} by XBOOLE_0:def 7;
A6: ((y `1) \/ (x `1)) /\ (x `2) = ((y `1) /\ (x `2)) \/ ((x `1) /\ (x `2)) by XBOOLE_1:23;
A7: ( (y \/ x) `1 = (y `1) \/ (x `1) & (y \/ x) `2 = (y `2) \/ (x `2) ) by MCART_1:7;

hereby :: thesis: ( ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} implies y \/ x in DISJOINT_PAIRS X )

assume y \/ x in DISJOINT_PAIRS X ; :: thesis: ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {}
then (y \/ x) `1 misses (y \/ x) `2 by Th42;
hence ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} by A5, A4, A7, A3, A6, XBOOLE_0:def 7; :: thesis: verum

end;

assume ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ; :: thesis: y \/ x in DISJOINT_PAIRS X
then (y \/ x) `1 misses (y \/ x) `2 by A5, A4, A7, A3, A6, XBOOLE_0:def 7;
hence y \/ x in DISJOINT_PAIRS X ; :: thesis: verum