let V be RealLinearSpace; for u, u1, v, v1, w, y being VECTOR of V holds
( [[u,v],[u1,v1]] in DTrapezium (V,w,y) iff u,v,u1,v1 are_DTr_wrt w,y )
let u, u1, v, v1, w, y be VECTOR of V; ( [[u,v],[u1,v1]] in DTrapezium (V,w,y) iff u,v,u1,v1 are_DTr_wrt w,y )
now ( [[u,v],[u1,v1]] in DTrapezium (V,w,y) implies u,v,u1,v1 are_DTr_wrt w,y )assume
[[u,v],[u1,v1]] in DTrapezium (
V,
w,
y)
;
u,v,u1,v1 are_DTr_wrt w,ythen consider u9,
v9,
u19,
v19 being
VECTOR of
V such that A1:
[u,v] = [u9,v9]
and A2:
[u1,v1] = [u19,v19]
and A3:
u9,
v9,
u19,
v19 are_DTr_wrt w,
y
by Def7;
A4:
u1 = u19
by A2, XTUPLE_0:1;
(
u = u9 &
v = v9 )
by A1, XTUPLE_0:1;
hence
u,
v,
u1,
v1 are_DTr_wrt w,
y
by A2, A3, A4, XTUPLE_0:1;
verum end;
hence
( [[u,v],[u1,v1]] in DTrapezium (V,w,y) iff u,v,u1,v1 are_DTr_wrt w,y )
by Def7; verum