let X, Y be set ; :: thesis: for R being Relation st X c= Y holds
R " X c= R " Y
let R be Relation; :: thesis: ( X c= Y implies R " X c= R " Y )
assume A1: X c= Y ; :: thesis: R " X c= R " Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in R " X or x in R " Y )
assume x in R " X ; :: thesis: x in R " Y
then ex y being object st
( [x,y] in R & y in X ) by Def12;
hence x in R " Y by A1, Def12; :: thesis: verum