let S be satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c being POINT of S st right_angle a,b,c & Collinear a,b,c & not a = b holds
c = b
let a, b, c be POINT of S; :: thesis: ( right_angle a,b,c & Collinear a,b,c & not a = b implies c = b )
assume A1: ( right_angle a,b,c & Collinear a,b,c ) ; :: thesis: ( a = b or c = b )
assume A2: a <> b ; :: thesis: c = b
Collinear b,a,c by A1, GTARSKI3:45;
hence c = b by A1, A2, Satz8p3, Satz8p8; :: thesis: verum