let POS be OrtAfSp; :: thesis: for K being Subset of
for a, b, c, d being Element of st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
let K be Subset of ; :: thesis: for a, b, c, d being Element of st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
let a, b, c, d be Element of ; :: thesis: ( a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b implies c,d _|_ K )
assume that
A1: a,b _|_ K and
A2: ( a,b // c,d or c,d // a,b ) and
A3: a <> b ; :: thesis: c,d _|_ K
reconsider a' = a, b' = b, c' = c, d' = d as Element of ;
consider p, q being Element of such that
A4: ( p <> q & K = Line p,q ) and
A5: a,b _|_ p,q by A1, Def14;
( a',b' // c',d' or c',d' // a',b' ) by A2, Th48;
then a',b' // c',d' by AFF_1:13;
then a,b // c,d by Th48;
then p,q _|_ c,d by A3, A5, Def9;
then c,d _|_ p,q by Def9;
hence c,d _|_ K by A4, Def14; :: thesis: verum