let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V st Gen w,y holds
AMSpace V,w,y is OrtAfPl
let w, y be VECTOR of V; :: thesis: ( Gen w,y implies AMSpace V,w,y is OrtAfPl )
assume A1: Gen w,y ; :: thesis: AMSpace V,w,y is OrtAfPl
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 _|_ r,s & not p,q // r,s implies a = b ) ) by A1, Th33, Th34, Th35, Th36, Th38, Th40;
A3: 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 A4: 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 ) ) & ( for w1 being VECTOR of V ex a, b being Real st w1 = (a * w) + (b * y) ) ) by A1, Def1;
then OASpace V is OAffinPlane by ANALOAF:51;
then AffinStruct(# the carrier of (AMSpace V,w,y),the CONGR of (AMSpace V,w,y) #) is AffinPlane by A4, DIRAF:53;
hence AMSpace V,w,y is OrtAfPl by A2, A3, Def10; :: thesis: verum