theorem Th01: :: GTARSKI4:37

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b, p, q being POINT of S st a <> b & a <> p & right_angle b,a,p & right_angle a,b,q holds
not Collinear p,a,q