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 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 ; :: thesis: ( a,x _|_ K & x in K )
thus a,x _|_ K by A1, A2, A3; :: thesis: x in K
thus x in K by A2, A4, Def10; :: thesis: verum