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 [*]

A2: field R1 c= field R2 by A1, RELAT_1:16;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in R1 [*] or p in R2 [*] )

assume A3: p in R1 [*] ; :: thesis: p in R2 [*]

consider x, y being object 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: for i being Nat st i >= 1 & i < len r holds

[(r . i),(r . (i + 1))] in R2 by A1, A6;

( 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

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 [*]

A2: field R1 c= field R2 by A1, RELAT_1:16;

let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in R1 [*] or p in R2 [*] )

assume A3: p in R1 [*] ; :: thesis: p in R2 [*]

consider x, y being object 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: for i being Nat st i >= 1 & i < len r holds

[(r . i),(r . (i + 1))] in R2 by A1, A6;

( 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