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