let POS be OrtAfSp; for A, K, M, N being Subset of POS
for a, b, p being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line holds
A _|_ K
let A, K, M, N be Subset of POS; for a, b, p being Element of POS st p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line holds
A _|_ K
let a, b, p be Element of POS; ( p in M & p in N & a in M & b in N & a <> b & a in K & b in K & A _|_ M & A _|_ N & K is being_line implies A _|_ K )
assume that
A1:
( p in M & p in N & a in M & b in N )
and
A2:
a <> b
and
A3:
( a in K & b in K )
and
A4:
A _|_ M
and
A5:
A _|_ N
and
A6:
K is being_line
; A _|_ K
A is being_line
by A4;
then consider q, r being Element of POS such that
A7:
q <> r
and
A8:
A = Line (q,r)
;
reconsider q9 = q, r9 = r as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
Line (q,r) = Line (q9,r9)
by Th41;
then
( q in A & r in A )
by A8, AFF_1:15;
then
( q,r _|_ p,a & q,r _|_ p,b )
by A1, A4, A5, Th56;
then A9:
q,r _|_ a,b
by Def7;
K = Line (a,b)
by A2, A3, A6, Th54;
hence
A _|_ K
by A2, A7, A8, A9, Th45; verum