let X be set ; :: thesis: for x being Element of [:(Fin X),(Fin X):]
for b being Element of DISJOINT_PAIRS X st x c= b holds
x is Element of DISJOINT_PAIRS X
let x be Element of [:(Fin X),(Fin X):]; :: thesis: for b being Element of DISJOINT_PAIRS X st x c= b holds
x is Element of DISJOINT_PAIRS X
let b be Element of DISJOINT_PAIRS X; :: thesis: ( x c= b implies x is Element of DISJOINT_PAIRS X )
assume A1: ( x `1 c= b `1 & x `2 c= b `2 ) ; :: according to NORMFORM:def 1 :: thesis: x is Element of DISJOINT_PAIRS X
b `1 misses b `2 by Th23;
then x `1 misses x `2 by A1, XBOOLE_1:64;
hence x is Element of DISJOINT_PAIRS X by Th23; :: thesis: verum