let C be AltCatStr ; :: thesis: ( C is quasi-discrete implies C is transitive )
assume A1: C is quasi-discrete ; :: thesis: C is transitive
let o1, o2, o3 be object of C; :: according to ALTCAT_1:def 4 :: thesis: ( <^o1,o2^> <> {} & <^o2,o3^> <> {} implies <^o1,o3^> <> {} )
assume ( <^o1,o2^> <> {} & <^o2,o3^> <> {} ) ; :: thesis: <^o1,o3^> <> {}
hence <^o1,o3^> <> {} by A1, Def20; :: thesis: verum