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 and
A4: K = Line p,q and
A5: r,s _|_ p,q by A1, Def14;
consider a, b, c, d being Element of POS such that
A6: a <> b and
A7: c <> d and
A8: K = Line a,b and
A9: M = Line c,d and
A10: a,b // c,d by A2, Def16;
reconsider p' = p, q' = q, a' = a, b' = b, c' = c, d' = d as Element of (Af POS) ;
A11: K = Line a',b' by A8, Th56;
A12: K = Line p',q' by A4, Th56;
then q' in K by AFF_1:26;
then A13: LIN a',b',q' by A11, AFF_1:def 2;
p' in K by A12, AFF_1:26;
then LIN a',b',p' by A11, AFF_1:def 2;
then A14: a',b' // p',q' by A13, AFF_1:19;
A15: p,q _|_ r,s by A5, Def9;
a',b' // c',d' by A10, Th48;
then p',q' // c',d' by A6, A14, AFF_1:14;
then p,q // c,d by Th48;
then r,s _|_ c,d by A3, A15, Def9;
hence r,s _|_ M by A7, A9, Def14; :: thesis: verum