let POS be OrtAfPl; :: thesis: for K being Subset of POS
for a, b being Element of POS st a,b _|_ K holds
ex p being Element of POS st
( LIN a,b,p & p in K )
let K be Subset of POS; :: thesis: for a, b being Element of POS st a,b _|_ K holds
ex p being Element of POS st
( LIN a,b,p & p in K )
let a, b be Element of POS; :: thesis: ( a,b _|_ K implies ex p being Element of POS st
( LIN a,b,p & p in K ) )
assume a,b _|_ K ; :: thesis: ex p being Element of POS st
( LIN a,b,p & p in K )
then consider p, q being Element of POS such that
p <> q and
A1: K = Line (p,q) and
A2: a,b _|_ p,q ;
consider c being Element of POS such that
A3: LIN a,b,c and
A4: LIN p,q,c by A2, Th67;
c in K by A1, A4, Def10;
hence ex p being Element of POS st
( LIN a,b,p & p in K ) by A3; :: thesis: verum