Hi Jon, You can rename it as you see fit! Adding a “d” is indeed the practice.
At first I misunderstood what you wanted to do. You want a theorem that states that if a surface has an area, so has a subset of that surface. Benoit is right, you will need additional conditions on you C for that, like probably ‘ C e. dom vol ‘ Note also that your set B can be written as ‘ B = ( A i^i ( C X. RR ) ) ‘. This is shorter and does not require a free variable. BR, _ Thierry -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/179A402A-E4EB-4147-81AB-F6DD8B74C361%40gmx.net.
