:: deftheorem Def1 defines with_pair FACIRC_1:def 2 :
for IT being set holds
( IT is with_pair iff ex x being pair object st x in IT );