let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
AMSpace (V,w,y) is OrtAfSp
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies AMSpace (V,w,y) is OrtAfSp )
set POS = AMSpace (V,w,y);
set X = AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #);
assume A1: Gen w,y ; :: thesis: AMSpace (V,w,y) is OrtAfSp
then A2: for a, b, c being Element of (AMSpace (V,w,y)) ex x being Element of (AMSpace (V,w,y)) st
( a,b _|_ c,x & c <> x ) by Th27;
A3: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V) by Th20;
for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 ) by A1;
then OASpace V is OAffinSpace by ANALOAF:26;
then A4: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) is AffinSpace by A3, DIRAF:41;
( ( for a, b, c, d, p, q, r, s being Element of (AMSpace (V,w,y)) holds
( ( a,b _|_ a,b implies a = b ) & a,b _|_ c,c & ( a,b _|_ c,d implies ( a,b _|_ d,c & c,d _|_ a,b ) ) & ( a,b _|_ p,q & a,b // r,s & not p,q _|_ r,s implies a = b ) & ( a,b _|_ p,q & a,b _|_ p,s implies a,b _|_ q,s ) ) ) & ( for a, b, c being Element of (AMSpace (V,w,y)) st a <> b holds
ex x being Element of (AMSpace (V,w,y)) st
( a,b // a,x & a,b _|_ x,c ) ) ) by A1, Th23, Th24, Th25, Th26, Th29, Th30, Th32;
hence AMSpace (V,w,y) is OrtAfSp by A2, A4, Def7; :: thesis: verum