environ
    given Fred being PERSON;
    A: Knight[Fred];
begin
            == This says the same as in the previous example.
            == But it tries to prove that all persons are knights!

    1: now
        let Fred be PERSON; == You can do it.

            == The following does not work as Fred mentioned in axiom A
            == is not the same Fred as inside this reasoning.

        thus Knight[Fred] by A;
****************************99
**
**  99 Your inference is not accepted by the checker.
**
    end;

    for p being PERSON holds Knight[Fred] by 1;                 == UI
********************************************99
**
**  99 Your inference is not accepted by the checker.
**

        == Note. The reasoning at 1 was incorrect, still we can make
        == a reference to it.
        == The above does not work, but the step below does.

    for Fred being PERSON holds Knight[Fred] by 1;              == UI