(* Inclusion ****************************************************************)
definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝
(* Inclusion ****************************************************************)
definition subR2 (S1) (S2): relation (relation2 S1 S2) ≝