let POS be OrtAfSp; 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; for r, s being Element of POS st r,s _|_ K & K // M holds
r,s _|_ M
let r, s be Element of POS; ( r,s _|_ K & K // M implies r,s _|_ M )
assume that
A1:
r,s _|_ K
and
A2:
K // M
; 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; verum