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 holds
ex d being Element of (DTrSpace (V,w,y)) st
( a,b // c,d or a,b // d,c )
let w, y be VECTOR of V; :: thesis: for a, b, c being Element of (DTrSpace (V,w,y)) st Gen w,y holds
ex d being Element of (DTrSpace (V,w,y)) st
( a,b // c,d or a,b // d,c )
let a, b, c be Element of (DTrSpace (V,w,y)); :: thesis: ( Gen w,y implies ex d being Element of (DTrSpace (V,w,y)) st
( a,b // c,d or a,b // d,c ) )
reconsider u = a, v = b, u1 = c as VECTOR of V ;
assume Gen w,y ; :: thesis: ex d being Element of (DTrSpace (V,w,y)) st
( a,b // c,d or a,b // d,c )
then consider t being VECTOR of V such that
A1: ( u,v,u1,t are_DTr_wrt w,y or u,v,t,u1 are_DTr_wrt w,y ) by Th20;
reconsider d = t as Element of (DTrSpace (V,w,y)) ;
( a,b // c,d or a,b // d,c ) by A1, Th44;
hence ex d being Element of (DTrSpace (V,w,y)) st
( a,b // c,d or a,b // d,c ) ; :: thesis: verum