let V be RealLinearSpace; :: thesis: for w, y, u, v, u1, v1 being VECTOR of V
for a, b, a1, b1 being Element of (DTrSpace V,w,y) st Gen w,y & u = a & v = b & u1 = a1 & v1 = b1 holds
( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y )
let w, y, u, v, u1, v1 be VECTOR of V; :: thesis: for a, b, a1, b1 being Element of (DTrSpace V,w,y) st Gen w,y & 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: ( Gen w,y & 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:
( Gen w,y & u = a & v = b & u1 = a1 & v1 = b1 )
; :: thesis: ( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y )
A2:
now assume
a,
b // a1,
b1
;
:: thesis: u,v,u1,v1 are_DTr_wrt w,ythen
[[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, Th44;
:: thesis: verum end;
now assume
u,
v,
u1,
v1 are_DTr_wrt w,
y
;
:: thesis: a,b // a1,b1then
[[a,b],[a1,b1]] in DTrapezium V,
w,
y
by A1, Th44;
hence
a,
b // a1,
b1
by ANALOAF:def 2;
:: thesis: verum end;
hence
( a,b // a1,b1 iff u,v,u1,v1 are_DTr_wrt w,y )
by A2; :: thesis: verum