let AS be AffinSpace; for a, b being Element of AS
for A being Subset of AS st A is being_line & a in A holds
( b in A iff a,b // A )
let a, b be Element of AS; for A being Subset of AS st A is being_line & a in A holds
( b in A iff a,b // A )
let A be Subset of AS; ( A is being_line & a in A implies ( b in A iff a,b // A ) )
assume that
A1:
A is being_line
and
A2:
a in A
; ( b in A iff a,b // A )
consider p, q being Element of AS such that
A3:
p <> q
and
A4:
A = Line (p,q)
by A1;
hereby ( a,b // A implies b in A )
assume
b in A
;
a,b // Athen
p,
q // a,
b
by A2, A3, A4, Th21;
then
a,
b // p,
q
by Th3;
hence
a,
b // A
by A3, A4;
verum
end;
assume
a,b // A
; b in A
then consider p, q being Element of AS such that
A5:
p <> q
and
A6:
A = Line (p,q)
and
A7:
a,b // p,q
;
p,q // a,b
by A7, Th3;
hence
b in A
by A2, A5, A6, Th21; verum