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

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