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