consider V0 being non trivial RealLinearSpace such that
A1: ex u, v, w being Element of V0 st
( ( for a, b, c being Real st ((a * u) + (b * v)) + (c * w) = 0. V0 holds
( a = 0 & b = 0 & c = 0 ) ) & ( for y being Element of V0 ex a, b, c being Real st y = ((a * u) + (b * v)) + (c * w) ) ) by Th16;
consider u0, v0, w0 being Element of V0 such that
A2: for a, b, c being Real st ((a * u0) + (b * v0)) + (c * w0) = 0. V0 holds
( a = 0 & b = 0 & c = 0 ) and
for y being Element of V0 ex a, b, c being Real st y = ((a * u0) + (b * v0)) + (c * w0) by A1;
take V0 ; :: thesis: V0 is up-3-dimensional
thus V0 is up-3-dimensional by A2, Def6; :: thesis: verum