let A be Subset of E; :: thesis: not A is proper
thus A = E ; :: according to SUBSET_1:def 6 :: thesis: verum