theorem Th7: :: AFVECT0:7
for AFV being WeakAffVect
for a, b, c, d being Element of AFV st a,b // c,d holds
b,a // d,c