thus {} = union {} by ZFMISC_1:2; :: according to ORDINAL1:def 6 :: thesis: verum