let S be non empty satisfying_Tarski-model TarskiGeometryStruct ; for A, B being Subset of S
for a, b being POINT of S st a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B holds
A = B
let A, B be Subset of S; for a, b being POINT of S st a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B holds
A = B
let a, b be POINT of S; ( a <> b & A is_line & a in A & b in A & B is_line & a in B & b in B implies A = B )
assume that
A1:
a <> b
and
A2:
A is_line
and
A3:
a in A
and
A4:
b in A
and
A5:
B is_line
and
A6:
a in B
and
A7:
b in B
; A = B
consider pa, qa being POINT of S such that
pa <> qa
and
A8:
A = Line (pa,qa)
by A2;
consider pb, qb being POINT of S such that
pb <> qb
and
A9:
B = Line (pb,qb)
by A5;
( Line (pa,qa) = Line (a,b) & Line (pb,qb) = Line (a,b) )
by A1, A3, A4, A8, A2, A6, A7, A9, A5, Satz6p18;
hence
A = B
by A8, A9; verum