Metamath Proof Explorer


Syntax definition cstrkg2d

Description: Extends class notation with the class of geometries fulfilling the planarity axioms.

Ref Expression
Assertion cstrkg2d class 𝒢 Tarski 2D