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 ;
TARSKI:def 3 ( 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 }
;
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;
verum
end;
hence
{ [a,b] where a, b is Element of R : a <= P,b } is Relation of R
; verum