let POS be OrtAfSp; :: thesis: for K being Subset of POS
for a, b, c, d being Element of POS st a,b _|_ K & ( a,b // c,d or c,d // a,b ) & a <> b holds
c,d _|_ K
let K be Subset of POS; :: thesis: for a, b, c, d being Element of POS 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 POS; :: 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 a9 = a, b9 = b, c9 = c, d9 = d as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
consider p, q being Element of POS such that
A4: ( p <> q & K = Line (p,q) ) and
A5: a,b _|_ p,q by A1;
( a9,b9 // c9,d9 or c9,d9 // a9,b9 ) by A2, Th36;
then a9,b9 // c9,d9 by AFF_1:4;
then a,b // c,d by Th36;
then p,q _|_ c,d by A3, A5, Def7;
then c,d _|_ p,q by Def7;
hence c,d _|_ K by A4; :: thesis: verum