thus [#] E = E ; :: according to SUBSET_1:def 6 :: thesis: verum