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 & not a,b // a # d,b # c holds
a,b // b # c,a # d
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 & not a,b // a # d,b # c holds
a,b // b # c,a # d
let a, b, c, d be Element of (DTrSpace (V,w,y)); :: thesis: ( Gen w,y & a,b // c,d & not a,b // a # d,b # c implies a,b // b # c,a # d )
assume that
A1: Gen w,y and
A2: a,b // c,d ; :: thesis: ( a,b // a # d,b # c or a,b // b # c,a # d )
reconsider u = a, v = b, u1 = c, v1 = d as VECTOR of V ;
u,v,u1,v1 are_DTr_wrt w,y by A2, Th44;
then A3: ( u,v,u # v1,v # u1 are_DTr_wrt w,y or u,v,v # u1,u # v1 are_DTr_wrt w,y ) by A1, Th27;
( a # d = u # v1 & b # c = v # u1 ) by Def8;
hence ( a,b // a # d,b # c or a,b // b # c,a # d ) by A3, Th44; :: thesis: verum