let POS be OrtAfSp; for M, N, K, A being Subset of POS
for p, a, b 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 M, N, K, A be Subset of POS; for p, a, b 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 p, a, b 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, Th62;
then consider q, r being Element of POS such that
A7:
q <> r
and
A8:
A = Line (q,r)
by Def13;
reconsider q9 = q, r9 = r as Element of (Af POS) ;
Line (q,r) = Line (q9,r9)
by Th56;
then
( q in A & r in A )
by A8, AFF_1:26;
then
( q,r _|_ p,a & q,r _|_ p,b )
by A1, A4, A5, Th78;
then A9:
q,r _|_ a,b
by Def9;
K = Line (a,b)
by A2, A3, A6, Th76;
hence
A _|_ K
by A2, A7, A8, A9, Th63; verum