let POS be OrtAfPl; for K, M, N being Subset of POS st M _|_ K & N _|_ K holds
M // N
let K, M, N be Subset of POS; ( M _|_ K & N _|_ K implies M // N )
assume that
A1:
M _|_ K
and
A2:
N _|_ K
; M // N
consider p1, q1, a, b being Element of POS such that
A3:
p1 <> q1
and
A4:
a <> b
and
A5:
K = Line (p1,q1)
and
A6:
M = Line (a,b)
and
A7:
p1,q1 _|_ a,b
by A1, Th45;
consider p2, q2, c, d being Element of POS such that
A8:
p2 <> q2
and
A9:
c <> d
and
A10:
K = Line (p2,q2)
and
A11:
N = Line (c,d)
and
A12:
p2,q2 _|_ c,d
by A2, Th45;
reconsider p19 = p1, p29 = p2, q19 = q1, q29 = q2 as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
A13: Line (p19,q19) =
Line (p2,q2)
by A5, A10, Th41
.=
Line (p29,q29)
by Th41
;
then
q29 in Line (p19,q19)
by AFF_1:15;
then A14:
LIN p19,q19,q29
by AFF_1:def 2;
p29 in Line (p19,q19)
by A13, AFF_1:15;
then
LIN p19,q19,p29
by AFF_1:def 2;
then
p19,q19 // p29,q29
by A14, AFF_1:10;
then
p1,q1 // p2,q2
by Th36;
then
a,b _|_ p2,q2
by A3, A7, Th62;
then
a,b // c,d
by A8, A12, Th63;
hence
M // N
by A4, A6, A9, A11; verum