set X = the non empty set ;
take BoolePoset the non empty set ; :: thesis: ( BoolePoset the non empty set is bounded & not BoolePoset the non empty set is trivial )
thus ( BoolePoset the non empty set is bounded & not BoolePoset the non empty set is trivial ) ; :: thesis: verum