set f = NATOrd ;
set g = RelIncl omega;
for a, b being object holds
( [a,b] in NATOrd iff [a,b] in RelIncl omega )
proof
let a, b be object ; :: thesis: ( [a,b] in NATOrd iff [a,b] in RelIncl omega )
hereby :: thesis: ( [a,b] in RelIncl omega implies [a,b] in NATOrd )
assume [a,b] in NATOrd ; :: thesis: [a,b] in RelIncl omega
then consider x, y being Element of NAT such that
A1: ( [a,b] = [x,y] & x <= y ) ;
( x = Segm x & y = Segm y ) ;
then x c= y by A1, NAT_1:39;
hence [a,b] in RelIncl omega by A1, WELLORD2:def 1; :: thesis: verum
end;
assume A2: [a,b] in RelIncl omega ; :: thesis: [a,b] in NATOrd
then reconsider aa = a, bb = b as Element of NAT by ZFMISC_1:87;
A4: aa c= bb by A2, WELLORD2:def 1;
( aa = Segm aa & bb = Segm bb ) ;
then aa <= bb by A4, NAT_1:39;
hence [a,b] in NATOrd ; :: thesis: verum
end;
hence NATOrd = RelIncl omega by RELAT_1:def 2; :: thesis: verum