defpred S₁[ object ] means A . $1 = 0 ;
consider Y being set such that
A1: for a being object holds
( a in Y iff ( a in P & S₁[a] ) ) from XBOOLE_0:sch 1();
( Y c= P & P c= P * ) by A1, Th9;
then Y c= P * ;
then reconsider Y = Y as Subset of (P *) ;
take Y ; :: thesis: for a being object holds
( a in Y iff ( a in P & A . a = 0 ) )
thus for a being object holds
( a in Y iff ( a in P & A . a = 0 ) ) by A1; :: thesis: verum