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