theorem Th23: :: ABCMIZ_1:23

Vars c= Rank omega