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)) #);
A1: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) = Lambda (OASpace V) by Th20;
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) ) ) ;
then OASpace V is OAffinPlane by ANALOAF:28;
then A3: AffinStruct(# the carrier of (AMSpace (V,w,y)), the CONGR of (AMSpace (V,w,y)) #) is AffinPlane by A1, DIRAF:45;
( ( 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, Th23, Th24, Th25, Th26, Th27, Th28, Th30;
hence AMSpace (V,w,y) is OrtAfPl by A3, Def8; :: thesis: verum