| (1) | p → q ∨ p | by ∨R1 |
| (2) | q → q ∨ p | by ∨R2 |
| (3) | p ∨ q → q ∨ p | from (1) and (2) by ∨L. |
| (∨R1) | ■∨ V(p // q ∨ p) |
| (∨R2) | ■∨ V(q // q ∨ p) |
| (∨L) | ■∨ V(V(Δ, p / r), V(Δ, q / r) // V(Δ, p ∨ q / r)) |
| (1) | □∨ V(p // p ∨ q) | from (∨R1) by Extension |
| (2) | □∨ V(q // p ∨ q) | from (∨R2) by Extension |
| (3) | □∨ V(V(Δ, p / r), V(Δ, q / r) // V(Δ, p ∨ q / r)) | from (∨L) by Extension |
| (4) | □∨ V(V(p / q ∨ p), V(q / q ∨ p) // V(p ∨ q / q ∨ p)) | from (3) by Schematic Instantiation |
| (5) | □∨ V(p ∨ q // q ∨ p) | from (1), (2) and (4) by Second-order Closure |