let a, b, c, d be Real; :: thesis: for u, v, w being Element of (TOP-REAL 3) st u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| holds
|{u,v,w}| = 0
let u, v, w be Element of (TOP-REAL 3); :: thesis: ( u = |[a,b,1]| & v = |[c,d,1]| & w = |[((a + c) / 2),((b + d) / 2),1]| implies |{u,v,w}| = 0 )
assume that
A1: u = |[a,b,1]| and
A2: v = |[c,d,1]| and
A3: w = |[((a + c) / 2),((b + d) / 2),1]| ; :: thesis: |{u,v,w}| = 0
A4: ( u `1 = a & u `2 = b & u `3 = 1 & v `1 = c & v `2 = d & v `3 = 1 & w `1 = (a + c) / 2 & w `2 = (b + d) / 2 & w `3 = 1 ) by A1, A2, A3, EUCLID_5:2;
|{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
.= ((((((a * d) * 1) - ((1 * d) * ((a + c) / 2))) - (((a * 1) * (b + d)) / 2)) + (((b * 1) * (a + c)) / 2)) - ((b * c) * 1)) + (((1 * c) * (b + d)) / 2) by A4 ;
hence |{u,v,w}| = 0 ; :: thesis: verum