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