defpred S1[ object , object ] means $1 = $2;
consider f being Function of [:A,A:],BOOLEAN such that
A1:
for x, y being object st x in A & y in A holds
( ( S1[x,y] implies f . (x,y) = TRUE ) & ( not S1[x,y] implies f . (x,y) = FALSE ) )
from NOMIN_4:sch 1();
take
f
; for a, b being object st a in A & b in A holds
( ( a = b implies f . (a,b) = TRUE ) & ( a <> b implies f . (a,b) = FALSE ) )
thus
for a, b being object st a in A & b in A holds
( ( a = b implies f . (a,b) = TRUE ) & ( a <> b implies f . (a,b) = FALSE ) )
by A1; verum