set M = { [a,b] where a, b is Element of R : a <= P,b } ;
{ [a,b] where a, b is Element of R : a <= P,b } c= [: the carrier of R, the carrier of R:]
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { [a,b] where a, b is Element of R : a <= P,b } or x in [: the carrier of R, the carrier of R:] )
assume x in { [a,b] where a, b is Element of R : a <= P,b } ; :: thesis: x in [: the carrier of R, the carrier of R:]
then consider a, b being Element of R such that
A1: ( x = [a,b] & a <= P,b ) ;
thus x in [: the carrier of R, the carrier of R:] by A1; :: thesis: verum
end;
hence { [a,b] where a, b is Element of R : a <= P,b } is Relation of R ; :: thesis: verum