let X, Y be set ; :: thesis: for R being Relation st X c= Y holds
Y |` (X |` R) = X |` R
let R be Relation; :: thesis: ( X c= Y implies Y |` (X |` R) = X |` R )
( X c= Y implies Y /\ X = X ) by XBOOLE_1:28;
hence ( X c= Y implies Y |` (X |` R) = X |` R ) by Th90; :: thesis: verum