set A = the non empty trivial Subset of S;
take the non empty trivial Subset of S ; :: thesis: ( the non empty trivial Subset of S is trivial & the non empty trivial Subset of S is proper )
thus ( the non empty trivial Subset of S is trivial & the non empty trivial Subset of S is proper ) ; :: thesis: verum