let x be set ; :: thesis: ( x is without_pairs & x is Relation-like implies x is empty )
assume A1: for a being pair object holds not a in x ; :: according to FACIRC_1:def 2 :: thesis: ( not x is Relation-like or x is empty )
assume A2: for a being object st a in x holds
ex y, z being object st a = [y,z] ; :: according to RELAT_1:def 1 :: thesis: x is empty
assume not x is empty ; :: thesis: contradiction
then reconsider X = x as non empty set ;
set a = the Element of X;
ex y, z being object st the Element of X = [y,z] by A2;
hence contradiction by A1; :: thesis: verum