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;
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;
reconsider p9 = p, q9 = q, a9 = a, b9 = b, c9 = c, d9 = d as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
A11: K = Line (a9,b9) by A8, Th41;
A12: K = Line (p9,q9) by A4, Th41;
then q9 in K by AFF_1:15;
then A13: LIN a9,b9,q9 by A11, AFF_1:def 2;
p9 in K by A12, AFF_1:15;
then LIN a9,b9,p9 by A11, AFF_1:def 2;
then A14: a9,b9 // p9,q9 by A13, AFF_1:10;
A15: p,q _|_ r,s by A5, Def7;
a9,b9 // c9,d9 by A10, Th36;
then p9,q9 // c9,d9 by A6, A14, AFF_1:5;
then p,q // c,d by Th36;
then r,s _|_ c,d by A3, A15, Def7;
hence r,s _|_ M by A7, A9; :: thesis: verum