let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, a1, b1, c1, d1 being Element of (DTrSpace (V,w,y)) st Gen w,y & a,b // a1,b1 & a,b // c1,d1 & a <> b holds
a1,b1 // c1,d1
let w, y be VECTOR of V; :: thesis: for a, b, a1, b1, c1, d1 being Element of (DTrSpace (V,w,y)) st Gen w,y & a,b // a1,b1 & a,b // c1,d1 & a <> b holds
a1,b1 // c1,d1
let a, b, a1, b1, c1, d1 be Element of (DTrSpace (V,w,y)); :: thesis: ( Gen w,y & a,b // a1,b1 & a,b // c1,d1 & a <> b implies a1,b1 // c1,d1 )
assume that
A1: Gen w,y and
A2: ( a,b // a1,b1 & a,b // c1,d1 ) and
A3: a <> b ; :: thesis: a1,b1 // c1,d1
reconsider u = a, v = b, u1 = a1, v1 = b1, u2 = c1, v2 = d1 as VECTOR of V ;
( u,v,u1,v1 are_DTr_wrt w,y & u,v,u2,v2 are_DTr_wrt w,y ) by A2, Th44;
then u1,v1,u2,v2 are_DTr_wrt w,y by A1, A3, Th19;
hence a1,b1 // c1,d1 by Th44; :: thesis: verum