take {} E ; :: thesis: {} E is proper
thus {} E <> E ; :: according to SUBSET_1:def 6 :: thesis: verum