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 and
A2: b in K and
A3: c,d _|_ K ; :: thesis: ( c,d _|_ a,b & a,b _|_ c,d )
consider p, q being Element of POS such that
A4: p <> q and
A5: K = Line (p,q) and
A6: c,d _|_ p,q by A3;
reconsider a9 = a, b9 = b, p9 = p, q9 = q as Element of AffinStruct(# the carrier of POS, the CONGR of POS #) ;
LIN p,q,b by A2, A5, Def10;
then A7: LIN p9,q9,b9 by Th40;
LIN p,q,a by A1, A5, Def10;
then LIN p9,q9,a9 by Th40;
then p9,q9 // a9,b9 by A7, AFF_1:10;
then A8: p,q // a,b by Th36;
p,q _|_ c,d by A6, Def7;
hence c,d _|_ a,b by A4, A8, Def7; :: thesis: a,b _|_ c,d
hence a,b _|_ c,d by Def7; :: thesis: verum