let B, C be Ordinal; :: thesis: ( On X c= B & ( for A being Ordinal st On X c= A holds
B c= A ) & On X c= C & ( for A being Ordinal st On X c= A holds
C c= A ) implies B = C )
assume ( On X c= B & ( for A being Ordinal st On X c= A holds
B c= A ) & On X c= C & ( for A being Ordinal st On X c= A holds
C c= A ) ) ; :: thesis: B = C
hence ( B c= C & C c= B ) ; :: according to XBOOLE_0:def 10 :: thesis: verum