let A be Subset of S; :: thesis: ( A is proper implies A is empty )
assume A is proper ; :: thesis: A is empty
then A1: A <> S ;
ex s being Element of S st S = {s} by SUBSET_1:46;
hence A is empty by A1, ZFMISC_1:33; :: thesis: verum