let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, c, c9 being POINT of S st a <> b & c <> c9 & ( c in Line (a,b) or c in Line (b,a) ) & ( c9 in Line (a,b) or c9 in Line (b,a) ) holds
( Line (c,c9) = Line (a,b) & Line (c,c9) = Line (b,a) & Line (c9,c) = Line (b,a) & Line (c9,c) = Line (a,b) )
let a, b, c, c9 be POINT of S; :: thesis: ( a <> b & c <> c9 & ( c in Line (a,b) or c in Line (b,a) ) & ( c9 in Line (a,b) or c9 in Line (b,a) ) implies ( Line (c,c9) = Line (a,b) & Line (c,c9) = Line (b,a) & Line (c9,c) = Line (b,a) & Line (c9,c) = Line (a,b) ) )
assume that
A1: a <> b and
A2: c <> c9 and
A3: ( c in Line (a,b) or c in Line (b,a) ) and
A4: ( c9 in Line (a,b) or c9 in Line (b,a) ) ; :: thesis: ( Line (c,c9) = Line (a,b) & Line (c,c9) = Line (b,a) & Line (c9,c) = Line (b,a) & Line (c9,c) = Line (a,b) )
Line (a,b) is_line by A1, GTARSKI3:def 11;
hence ( Line (c,c9) = Line (a,b) & Line (c,c9) = Line (b,a) & Line (c9,c) = Line (b,a) & Line (c9,c) = Line (a,b) ) by A3, A4, A2, GTARSKI3:87; :: thesis: verum