let R be Relation; :: thesis: ( R is complete implies ( R is confluent & R is strongly-normalizing ) )
assume ( R is confluent & R is strongly-normalizing ) ; :: according to REWRITE1:def 25 :: thesis: ( R is confluent & R is strongly-normalizing )
hence ( R is confluent & R is strongly-normalizing ) ; :: thesis: verum