let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; :: thesis: for a, b, x, y being POINT of S st a,b equal_line x,y holds
Line (a,b) = Line (x,y)
let a, b, x, y be POINT of S; :: thesis: ( a,b equal_line x,y implies Line (a,b) = Line (x,y) )
assume A1: a,b equal_line x,y ; :: thesis: Line (a,b) = Line (x,y)
Line (a,b) = Line (x,y)
proof
A2: Line (a,b) c= Line (x,y)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Line (a,b) or z in Line (x,y) )
assume z in Line (a,b) ; :: thesis: z in Line (x,y)
then consider z9 being POINT of S such that
A3: z = z9 and
A4: Collinear a,b,z9 ;
z9 on_line x,y by A1, A4, Thequiv1;
then Collinear x,y,z9 ;
hence z in Line (x,y) by A3; :: thesis: verum
end;
Line (x,y) c= Line (a,b)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Line (x,y) or z in Line (a,b) )
assume z in Line (x,y) ; :: thesis: z in Line (a,b)
then consider z9 being POINT of S such that
A5: z = z9 and
A6: Collinear x,y,z9 ;
z9 on_line a,b by A6, A1, Thequiv1;
then Collinear a,b,z9 ;
hence z in Line (a,b) by A5; :: thesis: verum
end;
hence Line (a,b) = Line (x,y) by A2; :: thesis: verum
end;
hence Line (a,b) = Line (x,y) ; :: thesis: verum