let POS be OrtAfPl; for M, K, N being Subset of st M _|_ K & N _|_ K holds
M // N
let M, K, N be Subset of ; ( 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 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, Th63;
consider p2, q2, c, d being Element of 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, Th63;
reconsider p1' = p1, p2' = p2, q1' = q1, q2' = q2 as Element of ;
A13: Line p1',q1' =
Line p2,q2
by A5, A10, Th56
.=
Line p2',q2'
by Th56
;
then
q2' in Line p1',q1'
by AFF_1:26;
then A14:
LIN p1',q1',q2'
by AFF_1:def 2;
p2' in Line p1',q1'
by A13, AFF_1:26;
then
LIN p1',q1',p2'
by AFF_1:def 2;
then
p1',q1' // p2',q2'
by A14, AFF_1:19;
then
p1,q1 // p2,q2
by Th48;
then
a,b _|_ p2,q2
by A3, A7, Th84;
then
a,b // c,d
by A8, A12, Th85;
hence
M // N
by A4, A6, A9, A11, Def16; verum