let V be RealLinearSpace; :: thesis: for o, u, v, w, u1, v1, w1, u2, v2, w2 being Element of V st not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep holds
u1,v1,w1 are_LinDep

let o, u, v, w, u1, v1, w1, u2, v2, w2 be Element of V; :: thesis: ( not o is zero & u,v,w are_Prop_Vect & u2,v2,w2 are_Prop_Vect & u1,v1,w1 are_Prop_Vect & o,u,v,w,u2,v2,w2 lie_on_an_angle & o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop & u,v2,w1 are_LinDep & u2,v,w1 are_LinDep & u,w2,v1 are_LinDep & w,u2,v1 are_LinDep & v,w2,u1 are_LinDep & w,v2,u1 are_LinDep implies u1,v1,w1 are_LinDep )
assume that
A1: not o is zero and
A2: u,v,w are_Prop_Vect and
A3: u2,v2,w2 are_Prop_Vect and
A4: u1,v1,w1 are_Prop_Vect and
A5: o,u,v,w,u2,v2,w2 lie_on_an_angle and
A6: o,u,v,w,u2,v2,w2 are_half_mutually_not_Prop and
A7: u,v2,w1 are_LinDep and
A8: u2,v,w1 are_LinDep and
A9: u,w2,v1 are_LinDep and
A10: w,u2,v1 are_LinDep and
A11: v,w2,u1 are_LinDep and
A12: w,v2,u1 are_LinDep ; :: thesis: u1,v1,w1 are_LinDep
A13: not u is zero by A2;
A14: not are_Prop u2,v2 by A6;
A15: not are_Prop o,v by A6;
A16: not are_Prop u,v by A6;
A17: o,u2,v2 are_LinDep by A5;
A18: ( not are_Prop o,w2 & not are_Prop u2,w2 ) by A6;
A19: not u2 is zero by A3;
A20: ( not are_Prop o,w & not are_Prop u,w ) by A6;
A21: o,u,w are_LinDep by A5;
A22: not are_Prop o,v2 by A6;
A23: o,u2,w2 are_LinDep by A5;
A24: not o,u,u2 are_LinDep by A5;
then A25: not are_Prop o,u by ANPROJ_1:12;
A26: not w is zero by A2;
then o,u,w are_Prop_Vect by ;
then consider a3, b3 being Real such that
A27: b3 * w = o + (a3 * u) and
a3 <> 0 and
A28: b3 <> 0 by A21, A20, A25, Th6;
A29: not are_Prop u2,o by ;
A30: not w2 is zero by A3;
then o,u2,w2 are_Prop_Vect by ;
then consider c3, d3 being Real such that
A31: d3 * w2 = o + (c3 * u2) and
c3 <> 0 and
A32: d3 <> 0 by A23, A18, A29, Th6;
A33: o,u,v are_LinDep by A5;
A34: not v2 is zero by A3;
then o,u2,v2 are_Prop_Vect by ;
then consider c2, d2 being Real such that
A35: d2 * v2 = o + (c2 * u2) and
A36: c2 <> 0 and
A37: d2 <> 0 by A17, A22, A14, A29, Th6;
A38: not v is zero by A2;
then o,u,v are_Prop_Vect by ;
then consider a2, b2 being Real such that
A39: b2 * v = o + (a2 * u) and
a2 <> 0 and
A40: b2 <> 0 by A33, A15, A16, A25, Th6;
set v9 = o + (a2 * u);
set w9 = o + (a3 * u);
set v29 = o + (c2 * u2);
set w29 = o + (c3 * u2);
A41: not o + (c2 * u2) is zero by ;
A42: not o + (a2 * u) is zero by ;
A43: not o + (a3 * u) is zero by ;
A44: not o + (c3 * u2) is zero by ;
A45: are_Prop w2,o + (c3 * u2) by ;
then A46: u,o + (c3 * u2),v1 are_LinDep by ;
A47: are_Prop v,o + (a2 * u) by ;
then A48: o + (a2 * u),o + (c3 * u2),u1 are_LinDep by ;
A49: are_Prop v2,o + (c2 * u2) by ;
then A50: u,o + (c2 * u2),w1 are_LinDep by ;
A51: are_Prop w,o + (a3 * u) by ;
then A52: o + (a3 * u),o + (c2 * u2),u1 are_LinDep by ;
not are_Prop u,v2
proof end;
then not are_Prop u,o + (c2 * u2) by ;
then consider A3, B3 being Real such that
A53: w1 = (A3 * u) + (B3 * (o + (c2 * u2))) by ;
not o,u2,v are_LinDep
proof end;
then not are_Prop v,w2 by ;
then not are_Prop o + (a2 * u),o + (c3 * u2) by A39, A40, A31, A32, Lm21;
then consider A1, B1 being Real such that
A55: u1 = (A1 * (o + (a2 * u))) + (B1 * (o + (c3 * u2))) by ;
not o,u,v2 are_LinDep
proof end;
then not are_Prop v2,w by ;
then not are_Prop o + (a3 * u),o + (c2 * u2) by A27, A28, A35, A37, Lm21;
then consider A19, B19 being Real such that
A57: u1 = (A19 * (o + (a3 * u))) + (B19 * (o + (c2 * u2))) by ;
A58: u1 = (((A1 + B1) * o) + ((A1 * a2) * u)) + ((B1 * c3) * u2) by ;
A59: not are_Prop v2,w2 by A6;
A60: not are_Prop v,w by A6;
A61: ( not are_Prop o + (a2 * u),o + (a3 * u) & not are_Prop o + (c2 * u2),o + (c3 * u2) )
proof
A62: now :: thesis: not are_Prop o + (c2 * u2),o + (c3 * u2)
assume are_Prop o + (c2 * u2),o + (c3 * u2) ; :: thesis: contradiction
then are_Prop v2,o + (c3 * u2) by ;
hence contradiction by A59, A45, ANPROJ_1:2; :: thesis: verum
end;
A63: now :: thesis: not are_Prop o + (a2 * u),o + (a3 * u)
assume are_Prop o + (a2 * u),o + (a3 * u) ; :: thesis: contradiction
then are_Prop v,o + (a3 * u) by ;
hence contradiction by A60, A51, ANPROJ_1:2; :: thesis: verum
end;
assume ( are_Prop o + (a2 * u),o + (a3 * u) or are_Prop o + (c2 * u2),o + (c3 * u2) ) ; :: thesis: contradiction
hence contradiction by A63, A62; :: thesis: verum
end;
not are_Prop u,w2
proof end;
then not are_Prop u,o + (c3 * u2) by ;
then consider A2, B2 being Real such that
A64: v1 = (A2 * u) + (B2 * (o + (c3 * u2))) by ;
u2,w,v1 are_LinDep by A10;
then A65: u2,o + (a3 * u),v1 are_LinDep by ;
not are_Prop u2,w by ;
then not are_Prop u2,o + (a3 * u) by ;
then consider A29, B29 being Real such that
A66: v1 = (A29 * u2) + (B29 * (o + (a3 * u))) by ;
A67: v1 = ((B2 * o) + (A2 * u)) + ((B2 * c3) * u2) by ;
A68: u2,o + (a2 * u),w1 are_LinDep by ;
not are_Prop u2,v by ;
then not are_Prop u2,o + (a2 * u) by ;
then consider A39, B39 being Real such that
A69: w1 = (A39 * u2) + (B39 * (o + (a2 * u))) by ;
A70: w1 = ((B3 * o) + (A3 * u)) + ((B3 * c2) * u2) by ;
v1 = ((B29 * o) + ((B29 * a3) * u)) + (A29 * u2) by ;
then A71: ( B2 = B29 & A2 = B29 * a3 ) by ;
w1 = ((B39 * o) + ((B39 * a2) * u)) + (A39 * u2) by ;
then A72: ( B3 = B39 & A3 = B39 * a2 ) by ;
A73: u1 = (((A19 + B19) * o) + ((A19 * a3) * u)) + ((B19 * c2) * u2) by ;
then A74: B1 * c3 = B19 * c2 by ;
( A1 + B1 = A19 + B19 & A1 * a2 = A19 * a3 ) by ;
then A75: A1 = (((a3 * c3) - (a3 * c2)) * (((a3 * c2) - (a2 * c2)) ")) * B1 by ;
set v19 = (o + (a3 * u)) + (c3 * u2);
set C2 = a2 * c2;
set C3 = - (a3 * c3);
set u19 = ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2);
set w19 = (o + (a2 * u)) + (c2 * u2);
A76: ((a2 * c2) * c3) + ((- (a3 * c3)) * c2) = (c2 * c3) * (a2 - a3) ;
( (a2 * c2) + (- (a3 * c3)) = (a2 * c2) - (a3 * c3) & ((a2 * c2) * a3) + ((- (a3 * c3)) * a2) = (a2 * a3) * (c2 - c3) ) ;
then ((1 * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2))) + ((a2 * c2) * ((o + (a3 * u)) + (c3 * u2)))) + ((- (a3 * c3)) * ((o + (a2 * u)) + (c2 * u2))) = 0. V by ;
then A77: ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),(o + (a3 * u)) + (c3 * u2),(o + (a2 * u)) + (c2 * u2) are_LinDep ;
A78: not v1 is zero by A4;
A79: B2 <> 0
proof
assume not B2 <> 0 ; :: thesis: contradiction
then v1 = (0. V) + (0 * (o + (c3 * u2))) by
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A78; :: thesis: verum
end;
v1 = B2 * ((o + (a3 * u)) + (c3 * u2)) by ;
then A80: are_Prop (o + (a3 * u)) + (c3 * u2),v1 by ;
A81: not w1 is zero by A4;
A82: B3 <> 0
proof
assume not B3 <> 0 ; :: thesis: contradiction
then w1 = (0. V) + (0 * (o + (c2 * u2))) by
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A81; :: thesis: verum
end;
w1 = B3 * ((o + (a2 * u)) + (c2 * u2)) by ;
then A83: are_Prop (o + (a2 * u)) + (c2 * u2),w1 by ;
A84: not u1 is zero by A4;
A85: B1 <> 0
proof
assume not B1 <> 0 ; :: thesis: contradiction
then u1 = (0. V) + (0 * (o + (c3 * u2))) by
.= (0. V) + (0. V) by RLVECT_1:10
.= 0. V by RLVECT_1:4 ;
hence contradiction by A84; :: thesis: verum
end;
u1 = (B1 * (((a3 * c2) - (a2 * c2)) ")) * (((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2)) by A36, A61, A58, A75, Lm26;
then are_Prop ((((a3 * c3) - (a2 * c2)) * o) + (((a2 * a3) * (c3 - c2)) * u)) + (((c2 * c3) * (a3 - a2)) * u2),u1 by ;
hence u1,v1,w1 are_LinDep by ; :: thesis: verum