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