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