set M = { [a,b] where a, b is Element of R : b in S } ;
A1: { [a,b] where a, b is Element of R : b in S } c= [: the carrier of R, the carrier of R:]

proof

let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in { [a,b] where a, b is Element of R : b in S } or o in [: the carrier of R, the carrier of R:] )
assume o in { [a,b] where a, b is Element of R : b in S } ; :: thesis: o in [: the carrier of R, the carrier of R:]
then ex a, b being Element of R st
( o = [a,b] & b in S ) ;
hence o in [: the carrier of R, the carrier of R:] ; :: thesis: verum

end;

for x being set holds
( x in { [a,b] where a, b is Element of R : b in S } iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) ;
hence ex b₁ being Subset of [: the carrier of R, the carrier of R:] st
for x being set holds
( x in b₁ iff ex a, b being Element of R st
( x = [a,b] & b in S ) ) by A1; :: thesis: verum