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

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