take TarskiEuclid2Space ; :: thesis: TarskiEuclid2Space is satisfying_Lower_Dimension_Axiom
thus TarskiEuclid2Space is satisfying_Lower_Dimension_Axiom ; :: thesis: verum