[mizar] A puzzle

[Andrzej Trybulec <trybulec@math.uwb.edu.pl>]

In a new submitted article - AFINSQ_1 (The Authors:Tsunetou, Bancerek,
Nakamura) the theorem Th2 says

theorem Th2:
   k <= n implies k = k /\ n

the next theorem has a straightforward justification:

theorem
  k = k /\ n implies k <= n by Th2;

("/\" is the new notation for the intersection of sets, and the von
Neuman construction is used in MML, so both are true)

Mizar does not allow, as a rule, to justify "alpha implies beta" by
"beta implies alpha" :-)

Why it works in this case?

Greetings,
Andrzej Trybulec

PS Enjoy it, the explanation will be sent later.