take omega --> 1 ; :: thesis: ( not omega --> 1 is empty & omega --> 1 is non-empty & omega --> 1 is infinite & omega --> 1 is with_cardinal_domain & omega --> 1 is natural-valued )
thus ( not omega --> 1 is empty & omega --> 1 is non-empty & omega --> 1 is infinite & omega --> 1 is with_cardinal_domain & omega --> 1 is natural-valued ) ; :: thesis: verum