let X, Y be set ; :: thesis: for P, R being Relation st P c= R & X c= Y holds
P " X c= R " Y
let P, R be Relation; :: thesis: ( P c= R & X c= Y implies P " X c= R " Y )
assume ( P c= R & X c= Y ) ; :: thesis: P " X c= R " Y
then ( P " X c= R " X & R " X c= R " Y ) by Th133, Th134;
hence P " X c= R " Y ; :: thesis: verum