let b1, b2 be epsilon Ordinal; :: thesis: ( a in b1 & ( for b being epsilon Ordinal st a in b holds
b1 c= b ) & a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) implies b1 = b2 )
assume that
A3: ( a in b1 & ( for b being epsilon Ordinal st a in b holds
b1 c= b ) ) and
A4: ( a in b2 & ( for b being epsilon Ordinal st a in b holds
b2 c= b ) ) ; :: thesis: b1 = b2
thus ( b1 c= b2 & b2 c= b1 ) by A3, A4; :: according to XBOOLE_0:def 10 :: thesis: verum