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