take [#] Y ; :: thesis: ( not [#] Y is trivial & not [#] Y is proper )
thus ( not [#] Y is trivial & not [#] Y is proper ) ; :: thesis: verum