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