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 set ; :: 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 consider x being set such that
A2: ( [x,y] in R & x in X ) by Def13;
thus y in R .: Y by A1, A2, Def13; :: thesis: verum