let AS be AffinSpace; for a, b, x being Element of AS
for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds
x in A
let a, b, x be Element of AS; for A being Subset of AS st A is being_line & a in A & b in A & a <> b & LIN a,b,x holds
x in A
let A be Subset of AS; ( A is being_line & a in A & b in A & a <> b & LIN a,b,x implies x in A )
assume that
A1:
A is being_line
and
A2:
a in A
and
A3:
b in A
and
A4:
a <> b
and
A5:
LIN a,b,x
; x in A
A = Line (a,b)
by A1, A2, A3, A4, Lm6;
hence
x in A
by A5, Def2; verum