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 object ; :: 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 ex s being Element of S st
( x = s & s |= f ) ;
hence x in S ; :: thesis: verum

end;

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