defpred S₁[ object ] means ( $1 in P & A . $1 = 0 );
let Y1, Y2 be Subset of (P *); :: thesis: ( ( for a being object holds
( a in Y1 iff ( a in P & A . a = 0 ) ) ) & ( for a being object holds
( a in Y2 iff ( a in P & A . a = 0 ) ) ) implies Y1 = Y2 )
assume that
A1: for a being object holds
( a in Y1 iff S₁[a] ) and
A2: for a being object holds
( a in Y2 iff S₁[a] ) ; :: thesis: Y1 = Y2
thus Y1 = Y2 from XBOOLE_0:sch 2(A1, A2); :: thesis: verum