Theorem txtopi

Description: The product of two topologies is a topology. (Contributed by Jeff Madsen, 15-Jun-2010)

	Ref	Expression
Hypotheses	txtopi.1	|- R e. Top
	txtopi.2	|- S e. Top
Assertion	txtopi	|- ( R tX S ) e. Top

Proof

Step	Hyp	Ref	Expression
1		txtopi.1	|- R e. Top
2		txtopi.2	|- S e. Top
3		txtop	|- ( ( R e. Top /\ S e. Top ) -> ( R tX S ) e. Top )
4	1 2 3	mp2an	|- ( R tX S ) e. Top