:: deftheorem defines right_angle GTARSKI4:def 1 :
for S being satisfying_CongruenceSymmetry satisfying_CongruenceEquivalenceRelation satisfying_CongruenceIdentity satisfying_SegmentConstruction satisfying_SAS satisfying_BetweennessIdentity TarskiGeometryStruct
for a, b, c being POINT of S holds
( right_angle a,b,c iff a,c equiv a, reflection (b,c) );