let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, c being Element of (DTrSpace (V,w,y)) st Gen w,y & a,b // b,c holds
( a = b & b = c )
let w, y be VECTOR of V; :: thesis: for a, b, c being Element of (DTrSpace (V,w,y)) st Gen w,y & a,b // b,c holds
( a = b & b = c )
let a, b, c be Element of (DTrSpace (V,w,y)); :: thesis: ( Gen w,y & a,b // b,c implies ( a = b & b = c ) )
assume that
A1: Gen w,y and
A2: a,b // b,c ; :: thesis: ( a = b & b = c )
reconsider u = a, v = b, u1 = c as VECTOR of V ;
u,v,v,u1 are_DTr_wrt w,y by A2, Th44;
hence ( a = b & b = c ) by A1, Th18; :: thesis: verum