let a be Element of X; :: thesis: a is ordinal

per cases ( X is empty or not X is empty ) ;

suppose X is empty ; :: thesis: a is ordinal

hence a is ordinal ; :: thesis: verum

end;

suppose not X is empty ; :: thesis: a is ordinal

hence a is ordinal by Th1; :: thesis: verum

end;

end;