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