let n, m be natural Ordinal; :: thesis: ( n divides m & m divides n implies n = m )
assume ( n divides m & m divides n ) ; :: thesis: n = m
then A1: ( m = n *^ (m div^ n) & n = m *^ (n div^ m) ) by Th11;
then A2: ( n *^ 1 = n & n = n *^ ((m div^ n) *^ (n div^ m)) ) by ORDINAL2:56, ORDINAL3:58;
A3: ( n = {} implies n = m ) by A1, ORDINAL2:52;
( (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:41;
hence n = m by A1, ORDINAL2:56; :: thesis: verum

end;

hence n = m by A2, A3, ORDINAL3:36; :: thesis: verum