scheme :: SCHEMS_1:sch 8
Schemat20b{ P1[ set ], P2[ set ] } :
ex a being set st
for b being set holds
( P1[a] or P2[b] )
provided
A1: for b being set ex a being set st
( P1[a] or P2[b] )