let R, Q be Relation; :: thesis: ( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) )
A1: (Q ~) ~ = Q ;
(R ~) ~ = R ;
hence ( ( R c= Q implies R ~ c= Q ~ ) & ( R ~ c= Q ~ implies R c= Q ) & ( R ~ c= Q implies R c= Q ~ ) & ( R c= Q ~ implies R ~ c= Q ) ) by A1, SYSREL:11; :: thesis: verum