theorem Satz6p11pb: :: GTARSKI3:79

for S being satisfying_Tarski-model TarskiGeometryStruct
for a, b, c, r, x, y being POINT of S st r <> a & b <> c & a out x,r & a,x equiv b,c & a out y,r & a,y equiv b,c holds
x = y