thus ( C is reflexive implies for o being Object of C holds <^o,o^> <> {} ) ; :: thesis: ( ( for o being Object of C holds <^o,o^> <> {} ) implies C is reflexive )
assume A1: for o being Object of C holds <^o,o^> <> {} ; :: thesis: C is reflexive
let x be set ; :: according to ALTCAT_2:def 6 :: thesis: ( x in the carrier of C implies the Arrows of C . (x,x) <> {} )
assume x in the carrier of C ; :: thesis: the Arrows of C . (x,x) <> {}
then reconsider o = x as Object of C ;
the Arrows of C . (x,x) = <^o,o^> ;
hence the Arrows of C . (x,x) <> {} by A1; :: thesis: verum