set NO = { [x,y] where x, y is Element of NAT : x <= y } ;

now :: thesis: for z being object st z in { [x,y] where x, y is Element of NAT : x <= y } holds
z in [:NAT,NAT:]

let z be object ; :: thesis: ( z in { [x,y] where x, y is Element of NAT : x <= y } implies z in [:NAT,NAT:] )
assume z in { [x,y] where x, y is Element of NAT : x <= y } ; :: thesis: z in [:NAT,NAT:]
then ex x, y being Element of NAT st
( z = [x,y] & x <= y ) ;
hence z in [:NAT,NAT:] ; :: thesis: verum

end;

hence { [x,y] where x, y is Element of NAT : x <= y } is Relation of NAT by TARSKI:def 3; :: thesis: verum