let x be set ; :: thesis: ( x is empty implies not x is with_pair )
assume A1: x is empty ; :: thesis: not x is with_pair
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