theorem :: GTARSKI3:142

for TP being Makarios_CE'2 holds TP is Makarios_CE2 ;