take <%omega,1%> ; :: thesis: ( not <%omega,1%> is trivial & <%omega,1%> is non-empty & <%omega,1%> is with_cardinal_domain & <%omega,1%> is Cardinal-yielding & not <%omega,1%> is natural-valued )
thus ( not <%omega,1%> is trivial & <%omega,1%> is non-empty & <%omega,1%> is with_cardinal_domain & <%omega,1%> is Cardinal-yielding & not <%omega,1%> is natural-valued ) ; :: thesis: verum