let A be Ordinal; :: thesis: ( A in 1 implies A = {} )
assume A in 1 ; :: thesis: A = {}
hence ( A c= {} & {} c= A ) by Lm1, ORDINAL1:22; :: according to XBOOLE_0:def 10 :: thesis: verum