theorem :: GTARSKI3:141

for TP being Makarios_CE2 holds TP is Makarios_CE'2 ;