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 )
set POS = AMSpace V,w,y;
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 A1: AffinStruct(# the carrier of (AMSpace V,w,y),the CONGR of (AMSpace V,w,y) #) = Lambda (OASpace V) by Th30;
assume A2: Gen w,y ; :: thesis: AMSpace V,w,y is OrtAfPl
then ( ( 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 Def1;
then OASpace V is OAffinPlane by ANALOAF:51;
then A3: AffinStruct(# the carrier of (AMSpace V,w,y),the CONGR of (AMSpace V,w,y) #) is AffinPlane by A1, DIRAF:53;
( ( 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 ) ) ) & ( 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 A2, Th33, Th34, Th35, Th36, Th37, Th38, Th40;
hence AMSpace V,w,y is OrtAfPl by A3, Def10; :: thesis: verum