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

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