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

A2: field R1 c= field R2 by A1, RELAT_1:16;
let p be set ; :: thesis: ( p in R1 [*] implies p in R2 [*] )
assume A3: p in R1 [*] ; :: thesis: p in R2 [*]
consider x, y being set such that
A4: p = [x,y] by A3, RELAT_1:def 1;
consider r being FinSequence such that
A5: ( len r >= 1 & 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 A3, A4, FINSEQ_1:def 16;

A7: now

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

end;

( x in field R1 & y in field R1 ) by A3, A4, FINSEQ_1:def 16;
hence p in R2 [*] by A4, A5, A2, A7, FINSEQ_1:def 16; :: thesis: verum

end;

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