take s1 ; :: thesis: s1 is s1 -reachable
thus TranslationRel S reduces s1,s1 by REWRITE1:12; :: according to MSAFREE5:def 33 :: thesis: verum