defpred S₁[ set ] means contradiction;
set X = the set ;
consider Y being set such that
A1: for x being set 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 set holds not x in Y by A1; :: according to XBOOLE_0:def 1 :: thesis: verum