:: deftheorem defines with_universal_friend FRIENDS1:def 2 :
for R being Relation holds
( R is with_universal_friend iff ex x being Element of field R st x is universal_friend );