let V be RealLinearSpace; :: thesis: for u, v, u1, 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, v, u1, v1, w, y be VECTOR of V; :: thesis: ( [[u,v],[u1,v1]] in DTrapezium V,w,y iff u,v,u1,v1 are_DTr_wrt w,y )
now assume
[[u,v],[u1,v1]] in DTrapezium V,
w,
y
;
:: thesis: u,v,u1,v1 are_DTr_wrt w,ythen consider u',
v',
u1',
v1' being
VECTOR of
V such that A1:
(
[u,v] = [u',v'] &
[u1,v1] = [u1',v1'] )
and A2:
u',
v',
u1',
v1' are_DTr_wrt w,
y
by Def7;
(
u = u' &
v = v' &
u1 = u1' &
v1 = v1' )
by A1, ZFMISC_1:33;
hence
u,
v,
u1,
v1 are_DTr_wrt w,
y
by A2;
:: thesis: verum end;
hence
( [[u,v],[u1,v1]] in DTrapezium V,w,y iff u,v,u1,v1 are_DTr_wrt w,y )
by Def7; :: thesis: verum