let X be set ; :: thesis: for x, y 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 x, y 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 ;
then A4: (x `1) /\ (x `2) = {} ;
y `1 misses y `2 by ;
then A5: (y `1) /\ (y `2) = {} ;
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) ) ;
thus ( y \/ x in DISJOINT_PAIRS X implies ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ) by ; :: thesis: ( ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} implies y \/ x in DISJOINT_PAIRS X )
assume ((y `1) /\ (x `2)) \/ ((x `1) /\ (y `2)) = {} ; :: thesis:
then (y \/ x) `1 misses (y \/ x) `2 by A5, A4, A3, A6;
hence y \/ x in DISJOINT_PAIRS X ; :: thesis: verum