let I be set ; :: thesis: ( I is natural-membered implies ( I is ordinal-membered & I is finite-membered ) )
assume A1: for a being object st a in I holds
a is natural ; :: according to MEMBERED:def 6 :: thesis: ( I is ordinal-membered & I is finite-membered )

now :: thesis: for J being set st J in I holds
J is ordinal

let J be set ; :: thesis: ( J in I implies J is ordinal )
assume J in I ; :: thesis: J is ordinal
then J is natural by A1;
hence J is ordinal ; :: thesis: verum

end;

hence I is ordinal-membered by ORDINAL6:1; :: thesis: I is finite-membered
let J be set ; :: according to FINSET_1:def 6 :: thesis: ( not J in I or J is finite )
assume J in I ; :: thesis: J is finite
then J is natural by A1;
hence J is finite ; :: thesis: verum