set P = { s where s is Element of S : s |= f } ;
{ s where s is Element of S : s |= f } c= S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of S : s |= f } or x in S )
assume x in { s where s is Element of S : s |= f } ; :: thesis: x in S
then consider s being Element of S such that
A1: x = s and
s |= f ;
thus x in S by A1; :: thesis: verum

end;

hence { s where s is Element of S : s |= f } is Subset of S ; :: thesis: verum