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