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