now :: thesis: for x, y being object st x in NAT & y in NAT & not [x,y] in NATOrd holds
[y,x] in NATOrd

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

proof

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

per cases ( x <= y or y <= x ) ;

suppose x <= y ; :: thesis: contradiction

hence contradiction by A3; :: thesis: verum

end;

suppose y <= x ; :: thesis: contradiction

hence contradiction by A4; :: thesis: verum

end;

end;

end;

end;

hence NATOrd is_strongly_connected_in NAT ; :: thesis: verum