scheme :: SCHEMS_1:sch 1
s1{ P₁[ set ] } :

ex b₁ being set st P₁[b₁]

provided

E1: for b₁ being set holds P₁[b₁]

proof end;

scheme :: SCHEMS_1:sch 2
s2{ P₁[ set , set ] } :

for b₁ being set ex b₂ being set st P₁[b₂,b₁]

provided

E1: ex b₁ being set st
for b₂ being set holds P₁[b₁,b₂]

proof end;

scheme :: SCHEMS_1:sch 3
s3{ P₁[ set ], P₂[ set ] } :

( ( for b₁ being set holds P₁[b₁] ) implies for b₁ being set holds P₂[b₁] )

provided

E1: for b₁ being set st P₁[b₁] holds
P₂[b₁]

proof end;

scheme :: SCHEMS_1:sch 4
s4{ P₁[ set ], P₂[ set ] } :

( ( for b₁ being set holds P₁[b₁] ) iff for b₁ being set holds P₂[b₁] )

provided

E1: for b₁ being set holds
( P₁[b₁] iff P₂[b₁] )

proof end;

scheme :: SCHEMS_1:sch 5
s5{ P₁[ set ], P₂[] } :

( ( for b₁ being set holds P₁[b₁] ) implies P₂[] )

provided

E1: for b₁ being set st P₁[b₁] holds
P₂[]

proof end;

scheme :: SCHEMS_1:sch 6
s6{ P₁[ set ], P₂[ set ] } :

ex b₁ being set st
for b₂ being set holds
( P₁[b₁] or P₂[b₂] )

provided

E1: ( ex b₁ being set st P₁[b₁] or for b₁ being set holds P₂[b₁] )

proof end;

scheme :: SCHEMS_1:sch 7
s7{ P₁[ set ], P₂[ set ] } :

( ex b₁ being set st P₁[b₁] or for b₁ being set holds P₂[b₁] )

provided

E1: ex b₁ being set st
for b₂ being set holds
( P₁[b₁] or P₂[b₂] )

proof end;

scheme :: SCHEMS_1:sch 8
s8{ P₁[ set ], P₂[ set ] } :

ex b₁ being set st
for b₂ being set holds
( P₁[b₁] or P₂[b₂] )

provided

E1: for b₁ being set ex b₂ being set st
( P₁[b₂] or P₂[b₁] )

proof end;

scheme :: SCHEMS_1:sch 9
s9{ P₁[ set ], P₂[ set ] } :

for b₁ being set ex b₂ being set st
( P₁[b₂] & P₂[b₁] )

provided

E1: ( ex b₁ being set st P₁[b₁] & ( for b₁ being set holds P₂[b₁] ) )

proof end;

scheme :: SCHEMS_1:sch 10
s10{ P₁[ set ], P₂[ set ] } :

( ex b₁ being set st P₁[b₁] & ( for b₁ being set holds P₂[b₁] ) )

provided

E1: for b₁ being set ex b₂ being set st
( P₁[b₂] & P₂[b₁] )

proof end;

scheme :: SCHEMS_1:sch 11
s11{ P₁[ set ], P₂[ set ] } :

ex b₁ being set st
for b₂ being set holds
( P₁[b₁] & P₂[b₂] )

provided

E1: for b₁ being set ex b₂ being set st
( P₁[b₂] & P₂[b₁] )

proof end;

scheme :: SCHEMS_1:sch 12
s12{ P₁[ set , set ] } :

ex b₁ being set st
for b₂ being set holds P₁[b₂,b₁]

provided

E1: for b₁, b₂ being set holds P₁[b₁,b₂]

proof end;

scheme :: SCHEMS_1:sch 13
s13{ P₁[ set , set ] } :

ex b₁ being set st P₁[b₁,b₁]

provided

E1: ex b₁ being set st
for b₂ being set holds P₁[b₁,b₂]

proof end;

scheme :: SCHEMS_1:sch 14
s14{ P₁[ set , set ] } :

for b₁ being set ex b₂ being set st P₁[b₂,b₁]

provided

E1: for b₁ being set holds P₁[b₁,b₁]

proof end;

scheme :: SCHEMS_1:sch 15
s15{ P₁[ set , set ] } :

for b₁ being set ex b₂ being set st P₁[b₁,b₂]

provided

E1: for b₁ being set holds P₁[b₁,b₁]

proof end;

scheme :: SCHEMS_1:sch 16
s16{ P₁[ set , set ] } :

ex b₁, b₂ being set st P₁[b₁,b₂]

provided

E1: for b₁ being set ex b₂ being set st P₁[b₂,b₁]

proof end;