theorem :: GTARSKI5:78

for S being non empty satisfying_Tarski-model satisfying_Lower_Dimension_Axiom TarskiGeometryStruct
for a, b being POINT of S
for A being Subset of S st A out2 a,b holds
A out2 b,a ;