let X be non empty set ; :: thesis: for R1, R2 being Relation of X st R1 c= R2 holds
R1 [*] c= R2 [*]
let R1, R2 be Relation of X; :: thesis: ( R1 c= R2 implies R1 [*] c= R2 [*] )
assume A1: R1 c= R2 ; :: thesis: R1 [*] c= R2 [*]

now

let p be set ; :: thesis: ( p in R1 [*] implies p in R2 [*] )
assume A2: p in R1 [*] ; :: thesis: p in R2 [*]
consider x, y being set such that
A3: p = [x,y] by A2, RELAT_1:def 1;
consider r being FinSequence such that
A4: len r >= 1 and
A5: ( r . 1 = x & r . (len r) = y ) and
A6: for i being Nat st i >= 1 & i < len r holds
[(r . i),(r . (i + 1))] in R1 by A2, A3, FINSEQ_1:def 16;
A7: ( x in field R1 & y in field R1 ) by A2, A3, FINSEQ_1:def 16;
A8: field R1 c= field R2 by A1, RELAT_1:31;

now

let i be Nat; :: thesis: ( i >= 1 & i < len r implies [(r . i),(r . (i + 1))] in R2 )
assume A9: ( i >= 1 & i < len r ) ; :: thesis: [(r . i),(r . (i + 1))] in R2
[(r . i),(r . (i + 1))] in R1 by A6, A9;
hence [(r . i),(r . (i + 1))] in R2 by A1; :: thesis: verum

end;

hence p in R2 [*] by A3, A4, A5, A7, A8, FINSEQ_1:def 16; :: thesis: verum

end;

hence R1 [*] c= R2 [*] by TARSKI:def 3; :: thesis: verum