:: deftheorem defines c= RELAT_1:def 3 :
for P being Relation
for A being set holds
( P c= A iff for a, b being object st [a,b] in P holds
[a,b] in A );