let POS be OrtAfSp; :: thesis: for K being Subset of POS
for a, b, c, d being Element of POS st a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds
c,d _|_ K
let K be Subset of POS; :: thesis: for a, b, c, d being Element of POS st a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) holds
c,d _|_ K
let a, b, c, d be Element of POS; :: thesis: ( a in K & b in K & a <> b & K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) implies c,d _|_ K )
assume that
A1: ( a in K & b in K & a <> b & K is being_line ) and
A2: ( a,b _|_ c,d or c,d _|_ a,b ) ; :: thesis: c,d _|_ K
A3: c,d _|_ a,b by A2, Def9;
K = Line a,b by A1, Th76;
hence c,d _|_ K by A1, A3, Def14; :: thesis: verum