:: deftheorem defines c= ORDINAL1:def 5 :
for A, B being Ordinal holds
( A c= B iff for C being Ordinal st C in A holds
C in B );