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