set P = { s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R ) } ;
{ s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R ) } c= S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in { s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R ) } or x in S )
assume x in { s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R ) } ; :: thesis: x in S
then consider s being Element of S such that
A1: x = s and
ex t being Element of S st
( t in H & [s,t] in R ) ;
thus x in S by A1; :: thesis: verum

end;

hence { s where s is Element of S : ex t being Element of S st
( t in H & [s,t] in R ) } is Subset of S ; :: thesis: verum