defpred S₁[ 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
( ( S₁[x,y] implies f . (x,y) = TRUE ) & ( not S₁[x,y] implies f . (x,y) = FALSE ) ) from NOMIN_4:sch 1();
take f ; :: thesis: 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; :: thesis: verum