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:]

hence
{ [x,y] where x, y is Element of NAT : x <= y } is Relation of NAT
by TARSKI:def 3; :: thesis: verumz 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;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