let POS be OrtAfPl; :: thesis: 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; :: thesis: 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; :: thesis: ( K is being_line implies ex x being Element of POS st
( a,x _|_ K & x in K ) )
assume K is being_line ; :: thesis: 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 & K = Line p,q ) by Def13;
consider x being Element of POS such that
A2: a,x _|_ p,q and
A3: LIN p,q,x by Th91;
take x ; :: thesis: ( a,x _|_ K & x in K )
thus a,x _|_ K by A1, A2, Def14; :: thesis: x in K
thus x in K by A1, A3, Def12; :: thesis: verum