:: deftheorem defines pairfree SCMYCIEL:def 3 :
for X being set holds
( X is pairfree iff PairsOf X is empty );