take Trivial-COM N ; :: thesis: ( Trivial-COM N is realistic & Trivial-COM N is strict )
thus ( Trivial-COM N is realistic & Trivial-COM N is strict ) ; :: thesis: verum