let A1, A2 be Ordinal; :: thesis: ( X c= Rank A1 & ( for B being Ordinal st X c= Rank B holds
A1 c= B ) & X c= Rank A2 & ( for B being Ordinal st X c= Rank B holds
A2 c= B ) implies A1 = A2 )
assume that
A2: ( X c= Rank A1 & ( for B being Ordinal st X c= Rank B holds
A1 c= B ) ) and
A3: ( X c= Rank A2 & ( for B being Ordinal st X c= Rank B holds
A2 c= B ) ) ; :: thesis: A1 = A2
thus ( A1 c= A2 & A2 c= A1 ) by A2, A3; :: according to XBOOLE_0:def 10 :: thesis: verum