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