let C1, C2 be category; :: thesis: ( not C1 [x] C2 is empty iff ( not C1 is empty & not C2 is empty ) )

hereby :: thesis: ( not C1 is empty & not C2 is empty implies not C1 [x] C2 is empty )

assume A1: not C1 [x] C2 is empty ; :: thesis: ( not C1 is empty & not C2 is empty )
pr1 (C1,C2) is covariant ;
hence not C1 is empty by A1, CAT_6:31; :: thesis: not C2 is empty
pr2 (C1,C2) is covariant ;
hence not C2 is empty by A1, CAT_6:31; :: thesis: verum

end;

assume A2: ( not C1 is empty & not C2 is empty ) ; :: thesis: not C1 [x] C2 is empty
reconsider C01 = C1 as non empty category by A2;
reconsider C02 = C2 as non empty category by A2;
set D = OrdC 1;
set G01 = the covariant Functor of (OrdC 1),C01;
set G02 = the covariant Functor of (OrdC 1),C02;
reconsider G1 = the covariant Functor of (OrdC 1),C01 as Functor of (OrdC 1),C1 ;
reconsider G2 = the covariant Functor of (OrdC 1),C02 as Functor of (OrdC 1),C2 ;
C1 [x] C2, pr1 (C1,C2), pr2 (C1,C2) is_product_of C1,C2 by Th48;
then consider H being Functor of (OrdC 1),(C1 [x] C2) such that
A3: ( H is covariant & (pr1 (C1,C2)) (*) H = G1 & (pr2 (C1,C2)) (*) H = G2 & ( for H1 being Functor of (OrdC 1),(C1 [x] C2) st H1 is covariant & (pr1 (C1,C2)) (*) H1 = G1 & (pr2 (C1,C2)) (*) H1 = G2 holds
H = H1 ) ) by Def17;
thus not C1 [x] C2 is empty by A3, CAT_6:31; :: thesis: verum