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