consider A being non empty trivial Subset of S;
take A ; :: thesis: ( A is trivial & A is proper )
thus ( A is trivial & A is proper ) ; :: thesis: verum