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 Def18;
hence the Comp of (DiscrCat A) . (o1,o2,o3) = {} ; :: thesis: verum