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 )
assume A1: Gen w,y ; :: thesis: AMSpace V,w,y is OrtAfSp
set POS = AMSpace V,w,y;
A2: 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 ) ) by A1, Th33, Th34, Th35, Th36, Th39, Th40;
A3: 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, Th42;
A4: 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 A1, Th37;
set X = AffinStruct(# the carrier of (AMSpace V,w,y),the CONGR of (AMSpace V,w,y) #);
AffinStruct(# the carrier of (AMSpace V,w,y),the CONGR of (AMSpace V,w,y) #) = Af (AMSpace V,w,y) ;
then A5: AffinStruct(# the carrier of (AMSpace V,w,y),the CONGR of (AMSpace V,w,y) #) = Lambda (OASpace V) by Th30;
for a, b being Real st (a * w) + (b * y) = 0. V holds
( a = 0 & b = 0 ) by A1, Def1;
then OASpace V is OAffinSpace by ANALOAF:38;
then AffinStruct(# the carrier of (AMSpace V,w,y),the CONGR of (AMSpace V,w,y) #) is AffinSpace by A5, DIRAF:48;
hence AMSpace V,w,y is OrtAfSp by A2, A3, A4, Def9; :: thesis: verum