let x be set ; :: thesis: ( x is empty implies x is without_pairs )
assume A1: x is empty ; :: thesis: x is without_pairs
let a be pair set ; :: according to FACIRC_1:def 2 :: thesis: not a in x
thus not a in x by A1; :: thesis: verum