let V be RealLinearSpace; :: thesis: for OAS being OAffinSpace st OAS = OASpace V holds
Lambda OAS is Moufangian
let OAS be OAffinSpace; :: thesis: ( OAS = OASpace V implies Lambda OAS is Moufangian )
assume OAS = OASpace V ; :: thesis: Lambda OAS is Moufangian
then Lambda OAS is Desarguesian by Th9, Th11;
hence Lambda OAS is Moufangian by Th15; :: thesis: verum