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 ) by Def13;
p,q _|_ a,a by Def9;
then a,a _|_ p,q by Def9;
hence a,a _|_ K by A1, Def14; :: thesis: verum