let U be Universe; :: thesis: for o, m being set st ( not m is U -set or not o is U -set ) holds
not 1Cat (o,m) is U -small
let o, m be set ; :: thesis: ( ( not m is U -set or not o is U -set ) implies not 1Cat (o,m) is U -small )
assume ( not m is U -set or not o is U -set ) ; :: thesis: not 1Cat (o,m) is U -small

per cases then ( not m is U -set or not o is U -set ) ;

suppose A1: not m is U -set ; :: thesis: not 1Cat (o,m) is U -small

1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) by CAT_1:def 11;
hence not 1Cat (o,m) is U -small by A1, Th18; :: thesis: verum

end;

suppose A2: not o is U -set ; :: thesis: not 1Cat (o,m) is U -small

1Cat (o,m) = CatStr(# {o},{m},(m :-> o),(m :-> o),((m,m) :-> m) #) by CAT_1:def 11;
hence not 1Cat (o,m) is U -small by A2, Th18; :: thesis: verum

end;

end;