∀x,y:ℝ. (rpositive(rmax(x;y))
rpositive(x) ∨ rpositive(y))
{ Auto }
1. x : ℝ@i
2. y : ℝ@i
3. rpositive(rmax(x;y))@i
⊢ rpositive(x) ∨ rpositive(y)
3. rpositive(x) ∨ rpositive(y)@i
⊢ rpositive(rmax(x;y))