let POS be OrtAfSp; :: thesis: for K, M being Subset of POS
for r, s being Element of POS st r,s _|_ K & K // M holds
r,s _|_ M
let K, M be Subset of POS; :: thesis: for r, s being Element of POS st r,s _|_ K & K // M holds
r,s _|_ M
let r, s be Element of POS; :: thesis: ( r,s _|_ K & K // M implies r,s _|_ M )
assume that
A1: r,s _|_ K and
A2: K // M ; :: thesis: r,s _|_ M
consider p, q being Element of POS such that
A3: ( p <> q & K = Line p,q & r,s _|_ p,q ) by A1, Def14;
consider a, b, c, d being Element of POS such that
A4: ( a <> b & c <> d ) and
A5: K = Line a,b and
A6: ( M = Line c,d & a,b // c,d ) by A2, Def16;
reconsider p' = p, q' = q, a' = a, b' = b, c' = c, d' = d as Element of the carrier of (Af POS) ;
A7: ( K = Line a',b' & K = Line p',q' ) by A3, A5, Th56;
then ( p' in K & q' in K ) by AFF_1:26;
then ( LIN a',b',p' & LIN a',b',q' ) by A7, AFF_1:def 2;
then A8: a',b' // p',q' by AFF_1:19;
a',b' // c',d' by A6, Th48;
then p',q' // c',d' by A4, A8, AFF_1:14;
then A9: p,q // c,d by Th48;
p,q _|_ r,s by A3, Def9;
then r,s _|_ c,d by A3, A9, Def9;
hence r,s _|_ M by A4, A6, Def14; :: thesis: verum