let C be non empty AltCatStr ; :: thesis: ( C is with_units implies C is reflexive )
assume A1: C is with_units ; :: thesis: C is reflexive
let o be object of C; :: according to ALTCAT_2:def 7 :: thesis: <^o,o^> <> {}
thus <^o,o^> <> {} by A1, ALTCAT_1:21; :: thesis: verum