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