defpred S₁[ object ] means contradiction;
consider Y being set such that
A1: for x being object holds
( x in Y iff ( x in the set & S₁[x] ) ) from XBOOLE_0:sch 1();
take Y ; :: thesis: Y is empty
thus for x being object holds not x in Y by A1; :: according to XBOOLE_0:def 1 :: thesis: verum