now :: thesis:

let x, y be object ; :: thesis:
assume that
A1: x in NAT and
A2: y in NAT ; :: thesis:
thus ( [x,y] in NATOrd or [y,x] in NATOrd ) :: thesis:

proof

assume that
A3: not [x,y] in NATOrd and
A4: not [y,x] in NATOrd ; :: thesis:
reconsider x = x, y = y as Element of NAT by A1, A2;

per cases ;

suppose x <= y ; :: thesis:

hence contradiction by A3; :: thesis:

end;

suppose y <= x ; :: thesis:

hence contradiction by A4; :: thesis:

end;

end;

end;

end;

hence NATOrd is_strongly_connected_in NAT ; :: thesis: