theorem :: GTARSKI3:141
for TP being Makarios_CE2 holds TP is Makarios_CE'2 ;