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

[y,x] in NATOrd

hence
NATOrd is_strongly_connected_in NAT
; :: thesis: verum[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

end;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