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 object ; :: 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 ex s being Element of S st
( x = s & ex t being Element of S st
( t in H & [s,t] in R ) ) ;
hence x in S ; :: 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