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 & c,d _|_ K holds
( c,d _|_ a,b & a,b _|_ c,d )
let K be Subset of POS; :: thesis: for a, b, c, d being Element of POS st a in K & b in K & c,d _|_ K holds
( c,d _|_ a,b & a,b _|_ c,d )
let a, b, c, d be Element of POS; :: thesis: ( a in K & b in K & c,d _|_ K implies ( c,d _|_ a,b & a,b _|_ c,d ) )
assume that
A1: ( a in K & b in K ) and
A2: c,d _|_ K ; :: thesis: ( c,d _|_ a,b & a,b _|_ c,d )
consider p, q being Element of POS such that
A3: ( p <> q & K = Line p,q & c,d _|_ p,q ) by A2, Def14;
reconsider a' = a, b' = b, p' = p, q' = q as Element of (Af POS) ;
( LIN p,q,a & LIN p,q,b ) by A1, A3, Def12;
then ( LIN p',q',a' & LIN p',q',b' ) by Th55;
then p',q' // a',b' by AFF_1:19;
then A4: p,q // a,b by Th48;
p,q _|_ c,d by A3, Def9;
hence c,d _|_ a,b by A3, A4, Def9; :: thesis: a,b _|_ c,d
hence a,b _|_ c,d by Def9; :: thesis: verum