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 and
A2: A = Line (b,c) by ANALMETR:def 12;
consider d being Element of X such that
A3: b,c _|_ a,d and
A4: a <> d by ANALMETR:39;
reconsider a9 = a, d9 = d as Element of AffinStruct(# the carrier of X, the CONGR of X #) ;
take K = Line (a,d); :: thesis: ( a in K & A _|_ K )
K = Line (a9,d9) by ANALMETR:41;
hence a in K by AFF_1:15; :: thesis: A _|_ K
thus A _|_ K by A1, A2, A3, A4, ANALMETR:45; :: thesis: verum