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 ) and
A2: a <> b and
A3: ( K is being_line & ( a,b _|_ c,d or c,d _|_ a,b ) ) ; :: thesis: c,d _|_ K
( c,d _|_ a,b & K = Line (a,b) ) by A1, A2, A3, Def7, Th54;
hence c,d _|_ K by A2; :: thesis: verum