take {} ; :: according to ARYTM_3:def 2 :: thesis: ex d1, d2 being Ordinal st
( {} = {} *^ d1 & {} = {} *^ d2 & not {} = 1 )
take {} ; :: thesis: ex d2 being Ordinal st
( {} = {} *^ {} & {} = {} *^ d2 & not {} = 1 )
take {} ; :: thesis: ( {} = {} *^ {} & {} = {} *^ {} & not {} = 1 )
thus ( {} = {} *^ {} & {} = {} *^ {} & not {} = 1 ) by ORDINAL2:35; :: thesis: verum