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