let A be Subset of E; :: thesis: ( not A is proper implies not A is empty )
assume A = E ; :: according to SUBSET_1:def 6 :: thesis: not A is empty
hence not A is empty ; :: thesis: verum