take BoolePoset {{}} ; :: thesis: ( not BoolePoset {{}} is trivial & BoolePoset {{}} is Boolean & BoolePoset {{}} is strict )
thus ( not BoolePoset {{}} is trivial & BoolePoset {{}} is Boolean & BoolePoset {{}} is strict ) ; :: thesis: verum