Metamath Proof Explorer
Table of Contents - 20.3.27. Elementary Geometry
- Two-dimensional geometry
- cstrkg2d
- df-trkg2d
- istrkg2d
- axtglowdim2ALTV
- axtgupdim2ALTV
- Morley's Miracle
- Outer Five Segment (not used, no need to move to main)
- cafs
- df-afs
- afsval
- brafs
- tg5segofs