:: deftheorem Def2 defines transitive ALTCAT_1:def 2 :
for G being AltGraph holds
( G is transitive iff for o1, o2, o3 being Object of G st <^o1,o2^> <> {} & <^o2,o3^> <> {} holds
<^o1,o3^> <> {} );