let A be non empty set ; :: thesis: for o1, o2, o3 being object of (DiscrCat A) st ( o1 <> o2 or o2 <> o3 ) holds
the Comp of (DiscrCat A) . o1,o2,o3 = {}
let o1, o2, o3 be object of (DiscrCat A); :: thesis: ( ( o1 <> o2 or o2 <> o3 ) implies the Comp of (DiscrCat A) . o1,o2,o3 = {} )
assume ( o1 <> o2 or o2 <> o3 ) ; :: thesis: the Comp of (DiscrCat A) . o1,o2,o3 = {}
then ( <^o1,o2^> = {} or <^o2,o3^> = {} ) by Def20;
then A1: [:<^o2,o3^>,<^o1,o2^>:] = {} ;
thus the Comp of (DiscrCat A) . o1,o2,o3 = {} by A1; :: thesis: verum