let POS be OrtAfPl; for K being Subset of POS
for a being Element of POS st K is being_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )
let K be Subset of POS; for a being Element of POS st K is being_line holds
ex x being Element of POS st
( a,x _|_ K & x in K )
let a be Element of POS; ( K is being_line implies ex x being Element of POS st
( a,x _|_ K & x in K ) )
assume
K is being_line
; ex x being Element of POS st
( a,x _|_ K & x in K )
then consider p, q being Element of POS such that
A1:
p <> q
and
A2:
K = Line (p,q)
;
consider x being Element of POS such that
A3:
a,x _|_ p,q
and
A4:
LIN p,q,x
by Th69;
take
x
; ( a,x _|_ K & x in K )
thus
a,x _|_ K
by A1, A2, A3; x in K
thus
x in K
by A2, A4, Def10; verum