let U be Universe; :: thesis: for o, m being object st 1Cat (o,m) is U -small holds
( m is U -set & o is U -set )
let o, m be object ; :: thesis: ( 1Cat (o,m) is U -small implies ( m is U -set & o is U -set ) )
reconsider o9 = o, m9 = m as set by TARSKI:1;
assume 1Cat (o,m) is U -small ; :: thesis: ( m is U -set & o is U -set )
then 1Cat (o9,m9) is U -small ;
hence ( m is U -set & o is U -set ) by Th94; :: thesis: verum