set R = the empty Relation;
set F = field the empty Relation;
for x, y being object st x in field the empty Relation & y in field the empty Relation & [x,y] in the empty Relation holds
[y,x] in the empty Relation ;
then A1: the empty Relation is symmetric by RELAT_2:def 3, RELAT_2:def 11;
for x being object st x in field the empty Relation holds
not [x,x] in the empty Relation ;
then A2: the empty Relation is irreflexive by RELAT_2:def 2, RELAT_2:def 10;
for x, y being object st x in field the empty Relation & y in field the empty Relation & x <> y holds
ex z being object st (Im ( the empty Relation,x)) /\ (Coim ( the empty Relation,y)) = {z} ;
hence ex b₁ being Relation st
( b₁ is finite & b₁ is symmetric & b₁ is irreflexive & b₁ is friendship_graph_like ) by A1, A2, Def3; :: thesis: verum