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 13;
consider d being Element of X such that
A3: b,c _|_ a,d and
A4: a <> d by ANALMETR:51;
reconsider a9 = a, d9 = d as Element of (Af X) by ANALMETR:47;
take K = Line a,d; :: thesis: ( a in K & A _|_ K )
K = Line a9,d9 by ANALMETR:56;
hence a in K by AFF_1:26; :: thesis: A _|_ K
thus A _|_ K by A1, A2, A3, A4, ANALMETR:63; :: thesis: verum