let x be Element of A; :: thesis: x is ordinal
( A is empty or not A is empty ) ;
hence x is ordinal by Th9, SUBSET_1:def 1; :: thesis: verum