let POS be OrtAfPl; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 & a <> b & M is being_line ) and
A2: ( c in N & d in N & c <> d & N is being_line ) and
A3: a,b // c,d ; :: thesis: M // N
( M = Line a,b & N = Line c,d ) by A1, A2, Th76;
hence M // N by A1, A2, A3, Def16; :: thesis: verum