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 ) 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 ; :: thesis: M // N
( M = Line (a,b) & N = Line (c,d) ) by A1, A2, A3, A4, A5, Th54;
hence M // N by A2, A4, A6; :: thesis: verum