theorem :: GTARSKI3:143

for TP being Makarios_CE2 holds
( TP is satisfying_Tarski-model & TP is satisfying_Lower_Dimension_Axiom & TP is satisfying_Upper_Dimension_Axiom & TP is satisfying_Euclid_Axiom & TP is satisfying_Continuity_Axiom ) ;