let POS be OrtAfSp; for K being Subset of POS
for a being Element of POS st K is being_line holds
a,a _|_ K
let K be Subset of POS; for a being Element of POS st K is being_line holds
a,a _|_ K
let a be Element of POS; ( K is being_line implies a,a _|_ K )
assume
K is being_line
; a,a _|_ K
then consider p, q being Element of POS such that
A1:
( p <> q & K = Line (p,q) )
;
p,q _|_ a,a
by Def7;
then
a,a _|_ p,q
by Def7;
hence
a,a _|_ K
by A1; verum