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