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 y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in R .: X or y in R .: Y )
assume y in R .: X ; :: thesis: y in R .: Y
then ex x being object st
( [x,y] in R & x in X ) by Def11;
hence y in R .: Y by A1, Def11; :: thesis: verum