Theorem Equiv.withBotCongr_trans

Modification history