let C be AltCatStr ; :: thesis: ( C is trivial & not C is empty implies C is quasi-discrete )
assume A1: ( C is trivial & not C is empty ) ; :: thesis: C is quasi-discrete
let i, j be object of C; :: according to ALTCAT_1:def 20 :: thesis: ( <^i,j^> <> {} implies i = j )
assume <^i,j^> <> {} ; :: thesis: i = j
thus i = j by A1, STRUCT_0:def 10; :: thesis: verum