let R, Q be Relation; :: thesis: ( R c= Q implies for p being RedSequence of R holds p is RedSequence of Q )
assume A1: R c= Q ; :: thesis: for p being RedSequence of R holds p is RedSequence of Q
let p be RedSequence of R; :: thesis: p is RedSequence of Q
thus len p > 0 ; :: according to REWRITE1:def 2 :: thesis: for i being Nat st i in dom p & i + 1 in dom p holds
[(p . i),(p . (i + 1))] in Q
let i be Nat; :: thesis: ( i in dom p & i + 1 in dom p implies [(p . i),(p . (i + 1))] in Q )
assume ( i in dom p & i + 1 in dom p ) ; :: thesis: [(p . i),(p . (i + 1))] in Q
then [(p . i),(p . (i + 1))] in R by Def2;
hence [(p . i),(p . (i + 1))] in Q by A1; :: thesis: verum