set X = the non empty trivial proper Subset of Y;
reconsider X = the non empty trivial proper Subset of Y as Subset of Y ;
take X ; :: thesis: ( not X is empty & X is trivial & X is proper )
thus ( not X is empty & X is trivial & X is proper ) ; :: thesis: verum