theorem Th20: :: ANALORT:20

for V being RealLinearSpace
for u, v, w, x, y being VECTOR of V holds u,u,v,w are_COrte_wrt x,y by ANALOAF:9;