let R, S be Relation; :: thesis: ( R c= S implies R ~ c= S ~ )
assume R c= S ; :: thesis: R ~ c= S ~
then R \/ S = S by XBOOLE_1:12;
then (R ~) \/ (S ~) = S ~ by RELAT_1:23;
hence R ~ c= S ~ by XBOOLE_1:7; :: thesis: verum