theorem :: SYSREL:11

for R, S being Relation st R c= S holds
R ~ c= S ~