let F be Function; :: thesis: ( F is empty implies F is nonpair-yielding )
assume A1: F is empty ; :: thesis: F is nonpair-yielding
let x be set ; :: according to FACIRC_1:def 3 :: thesis: ( not x in proj1 F or not F . x is pair )
assume x in dom F ; :: thesis: not F . x is pair
thus not F . x is pair by A1; :: thesis: verum