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

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