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 ( y in DISJOINT_PAIRS X & x in DISJOINT_PAIRS X ) ; :: thesis: ( y \/ x in DISJOINT_PAIRS X iff ((y `1 ) /\ (x `2 )) \/ ((x `1 ) /\ (y `2 )) = {} )
then ( y `1 misses y `2 & x `1 misses x `2 ) by Th42;
then A1: ( (y `1 ) /\ (y `2 ) = {} & (x `1 ) /\ (x `2 ) = {} ) by XBOOLE_0:def 7;
A2: ( (y \/ x) `1 = (y `1 ) \/ (x `1 ) & (y \/ x) `2 = (y `2 ) \/ (x `2 ) ) by MCART_1:7;
A3: ((y `1 ) \/ (x `1 )) /\ ((y `2 ) \/ (x `2 )) = (((y `1 ) \/ (x `1 )) /\ (y `2 )) \/ (((y `1 ) \/ (x `1 )) /\ (x `2 )) by XBOOLE_1:23;
A4: ( ((y `1 ) \/ (x `1 )) /\ (y `2 ) = ((y `1 ) /\ (y `2 )) \/ ((x `1 ) /\ (y `2 )) & ((y `1 ) \/ (x `1 )) /\ (x `2 ) = ((y `1 ) /\ (x `2 )) \/ ((x `1 ) /\ (x `2 )) ) by XBOOLE_1:23;

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 A1, A2, A3, A4, 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 A1, A2, A3, A4, XBOOLE_0:def 7;
hence y \/ x in DISJOINT_PAIRS X ; :: thesis: verum