let POS be OrtAfSp; :: thesis: 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; :: thesis: for a being Element of POS st K is being_line holds
a,a _|_ K
let a be Element of POS; :: thesis: ( K is being_line implies a,a _|_ K )
assume K is being_line ; :: thesis: 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; :: thesis: verum