let X be OrtAfPl; :: thesis: for A being Subset of X
for a being Element of X st A is being_line holds
ex K being Subset of X st
( a in K & A _|_ K )
let A be Subset of X; :: thesis: for a being Element of X st A is being_line holds
ex K being Subset of X st
( a in K & A _|_ K )
let a be Element of X; :: thesis: ( A is being_line implies ex K being Subset of X st
( a in K & A _|_ K ) )
assume A is being_line ; :: thesis: ex K being Subset of X st
( a in K & A _|_ K )
then consider b, c being Element of X such that
A1: ( b <> c & A = Line b,c ) by ANALMETR:def 13;
consider d being Element of X such that
A2: ( b,c _|_ a,d & a <> d ) by ANALMETR:51;
take K = Line a,d; :: thesis: ( a in K & A _|_ K )
reconsider a' = a, d' = d as Element of (Af X) by ANALMETR:47;
K = Line a',d' by ANALMETR:56;
hence a in K by AFF_1:26; :: thesis: A _|_ K
thus A _|_ K by A1, A2, ANALMETR:63; :: thesis: verum