let V be RealLinearSpace; :: thesis: for w, y, u, v being VECTOR of V st Gen w,y holds
u,v,u,v are_DTr_wrt w,y
let w, y, u, v be VECTOR of V; :: thesis: ( Gen w,y implies u,v,u,v are_DTr_wrt w,y )
assume A1: Gen w,y ; :: thesis: u,v,u,v are_DTr_wrt w,y
A2: u,v // u,v by ANALOAF:17;
u,v,u # v,u # v are_Ort_wrt w,y by A1, Lm5;
hence u,v,u,v are_DTr_wrt w,y by A2, Def3; :: thesis: verum