:: deftheorem defines _eq_ PRSUBSET:def 4 :
for a, b being object holds a _eq_ b = IFEQ (a,b,TRUE,FALSE);