let V be RealLinearSpace; :: thesis: for w, y being VECTOR of V
for a, b, c, d being Element of (DTrSpace V,w,y) st Gen w,y & a,b // c,d holds
( c,d // a,b & b,a // d,c )
let w, y be VECTOR of V; :: thesis: for a, b, c, d being Element of (DTrSpace V,w,y) st Gen w,y & a,b // c,d holds
( c,d // a,b & b,a // d,c )
let a, b, c, d be Element of (DTrSpace V,w,y); :: thesis: ( Gen w,y & a,b // c,d implies ( c,d // a,b & b,a // d,c ) )
assume A1: ( Gen w,y & a,b // c,d ) ; :: thesis: ( c,d // a,b & b,a // d,c )
reconsider u = a, v = b, u1 = c, v1 = d as VECTOR of V ;
u,v,u1,v1 are_DTr_wrt w,y by A1, Th47;
then ( v,u,v1,u1 are_DTr_wrt w,y & u1,v1,u,v are_DTr_wrt w,y ) by A1, Th23, Th24;
hence ( c,d // a,b & b,a // d,c ) by A1, Th47; :: thesis: verum