take Trivial-AMI N ; :: thesis: ( Trivial-AMI N is regular & Trivial-AMI N is J/A-independent )
thus ( Trivial-AMI N is regular & Trivial-AMI N is J/A-independent ) ; :: thesis: verum