theorem th0k: :: FIELD_5:3

for n, m being Nat holds
( ( n c= m implies n <= m ) & ( n <= m implies n c= m ) & ( n in m implies n < m ) & ( n < m implies n in m ) )