let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for A being Subset of S
for a, b being POINT of S st A is_line & a <> b & a in A & b in A holds
A = Line (a,b)
let A be Subset of S; for a, b being POINT of S st A is_line & a <> b & a in A & b in A holds
A = Line (a,b)
let a, b be POINT of S; ( A is_line & a <> b & a in A & b in A implies A = Line (a,b) )
assume that
A1:
A is_line
and
A2:
a <> b
and
A3:
a in A
and
A4:
b in A
; A = Line (a,b)
consider p, q being POINT of S such that
A5:
p <> q
and
A6:
A = Line (p,q)
by A1;
consider xa being POINT of S such that
A7:
a = xa
and
A8:
Collinear p,q,xa
by A3, A6;
consider xb being POINT of S such that
A9:
b = xb
and
A10:
Collinear p,q,xb
by A4, A6;
( a on_line p,q & b on_line p,q )
by A5, A7, A8, A9, A10;
hence
A = Line (a,b)
by A2, A6, Thequiv2, GTARSKI1:46; verum