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