let n, m be natural Ordinal; :: thesis: ( n divides m & m divides n implies n = m )
assume that
A1: n divides m and
A2: m divides n ; :: thesis: n = m
A3: m = n *^ (m div^ n) by A1, Th7;
A4: ( (m div^ n) *^ (n div^ m) = 1 implies n = m )

proof

assume (m div^ n) *^ (n div^ m) = 1 ; :: thesis: n = m
then m div^ n = 1 by ORDINAL3:37;
hence n = m by A3, ORDINAL2:39; :: thesis: verum

end;

n = m *^ (n div^ m) by A2, Th7;
then A5: ( n *^ 1 = n & n = n *^ ((m div^ n) *^ (n div^ m)) ) by A3, ORDINAL2:39, ORDINAL3:50;
( n = {} implies n = m ) by A3, ORDINAL2:35;
hence n = m by A5, A4, ORDINAL3:33; :: thesis: verum