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