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 ( {} 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 ) ) ; :: thesis: B = C
hence ( B c= C & C c= B ) ; :: according to XBOOLE_0:def 10 :: thesis: verum