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, XBOOLE_1:2; :: according to XBOOLE_0:def 10 :: thesis: verum