let u, v, w be Element of (TOP-REAL 3); :: thesis: ( v `3 = 0 & w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| implies |{u,v,w}| = 0 )
assume that
A2: v `3 = 0 and
A3: w = |[((u `1) + (v `1)),((u `2) + (v `2)),(u `3)]| ; :: thesis: |{u,v,w}| = 0
A4: |{u,v,w}| = (((((((u `1) * (v `2)) * (w `3)) - (((u `3) * (v `2)) * (w `1))) - (((u `1) * (v `3)) * (w `2))) + (((u `2) * (v `3)) * (w `1))) - (((u `2) * (v `1)) * (w `3))) + (((u `3) * (v `1)) * (w `2)) by ANPROJ_8:27
.= (((((u `1) * (v `2)) * (w `3)) - (((u `3) * (v `2)) * (w `1))) - (((u `2) * (v `1)) * (w `3))) + (((u `3) * (v `1)) * (w `2)) by A2 ;
( w `1 = (u `1) + (v `1) & w `2 = (u `2) + (v `2) & w `3 = u `3 ) by A3, EUCLID_5:2;
hence |{u,v,w}| = 0 by A4; :: thesis: verum