Theorem areage0

Description: The area of a measurable region is greater than or equal to zero. (Contributed by Mario Carneiro, 21-Jun-2015)

	Ref	Expression
Assertion	areage0	|- ( S e. dom area -> 0 <_ ( area ` S ) )

Proof

Step	Hyp	Ref	Expression
1		areaf	|- area : dom area --> ( 0 [,) +oo )
2	1	ffvelrni	|- ( S e. dom area -> ( area ` S ) e. ( 0 [,) +oo ) )
3		elrege0	|- ( ( area ` S ) e. ( 0 [,) +oo ) <-> ( ( area ` S ) e. RR /\ 0 <_ ( area ` S ) ) )
4	3	simprbi	|- ( ( area ` S ) e. ( 0 [,) +oo ) -> 0 <_ ( area ` S ) )
5	2 4	syl	|- ( S e. dom area -> 0 <_ ( area ` S ) )