let POS be OrtAfPl; for M, N being Subset of POS
for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d holds
M // N
let M, N be Subset of POS; for a, b, c, d being Element of POS st a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d holds
M // N
let a, b, c, d be Element of POS; ( a in M & b in M & a <> b & M is being_line & c in N & d in N & c <> d & N is being_line & a,b // c,d implies M // N )
assume that
A1:
( a in M & b in M )
and
A2:
a <> b
and
A3:
( M is being_line & c in N & d in N )
and
A4:
c <> d
and
A5:
N is being_line
and
A6:
a,b // c,d
; M // N
( M = Line (a,b) & N = Line (c,d) )
by A1, A2, A3, A4, A5, Th54;
hence
M // N
by A2, A4, A6; verum