let B, C be set ; :: thesis: ( {} in B & B is limit_ordinal & B is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
B c= A ) & {} in C & C is limit_ordinal & C is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
C c= A ) implies B = C )
assume that
A2: ( {} in B & B is limit_ordinal & B is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
B c= A ) ) and
A3: ( {} in C & C is limit_ordinal & C is ordinal & ( for A being Ordinal st {} in A & A is limit_ordinal holds
C c= A ) ) ; :: thesis: B = C
thus ( B c= C & C c= B ) by A2, A3; :: according to XBOOLE_0:def 10 :: thesis: verum