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,y
then 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, ZFMISC_1:27;
( u = u9 & v = v9 ) by A1, ZFMISC_1:27;
hence u,v,u1,v1 are_DTr_wrt w,y by A2, A3, A4, ZFMISC_1:27; :: 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