let V be RealLinearSpace; :: thesis: for u, u1, v, v1, w, y being VECTOR of V
for a, b, a1, b1 being Element of (DTrSpace (V,w,y)) st u = a & v = b & u1 = a1 & v1 = b1 holds
( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y )
let u, u1, v, v1, w, y be VECTOR of V; :: thesis: for a, b, a1, b1 being Element of (DTrSpace (V,w,y)) st u = a & v = b & u1 = a1 & v1 = b1 holds
( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y )
let a, b, a1, b1 be Element of (DTrSpace (V,w,y)); :: thesis: ( u = a & v = b & u1 = a1 & v1 = b1 implies ( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y ) )
assume A1: ( u = a & v = b & u1 = a1 & v1 = b1 ) ; :: thesis: ( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y )
hereby :: thesis: ( u,v,u1,v1 are_DTr_wrt w,y implies a,b // a1,b1 )
assume a,b // a1,b1 ; :: thesis: u,v,u1,v1 are_DTr_wrt w,y
then [[a,b],[a1,b1]] in DTrapezium (V,w,y) by ANALOAF:def 2;
hence u,v,u1,v1 are_DTr_wrt w,y by A1, Th42; :: thesis: verum
end;
assume u,v,u1,v1 are_DTr_wrt w,y ; :: thesis: a,b // a1,b1
then [[a,b],[a1,b1]] in DTrapezium (V,w,y) by A1, Th42;
hence a,b // a1,b1 by ANALOAF:def 2; :: thesis: verum