let X, x, y, z be set ; :: thesis: for TS being transition-system of X st x,y -->. z,TS holds
( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
let TS be transition-system of X; :: thesis: ( x,y -->. z,TS implies ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS ) )
assume x,y -->. z,TS ; :: thesis: ( x in TS & y in X & z in TS & x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
then A1: [[x,y],z] in the Tran of TS by Def2;
then [x,y] in [: the carrier of TS,X:] by ZFMISC_1:106;
hence ( x in the carrier of TS & y in X & z in the carrier of TS ) by A1, ZFMISC_1:106; :: according to STRUCT_0:def 5 :: thesis: ( x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) & z in rng the Tran of TS )
[x,y] in dom the Tran of TS by A1, RELAT_1:20;
hence ( x in dom (dom the Tran of TS) & y in rng (dom the Tran of TS) ) by RELAT_1:20; :: thesis: z in rng the Tran of TS
thus z in rng the Tran of TS by A1, RELAT_1:20; :: thesis: verum