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

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