Theorem isOpen_Ioi

Modification history