:: Schemes
:: by Stanis\l aw T. Czuba
::
:: Received December 17, 1990
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

scheme :: SCHEMS_1:sch 1
Schemat0{ P1[ set ] } :
 ex a being set st P1[a]
provided
A1: for a being set holds P1[a]
proofend;

scheme :: SCHEMS_1:sch 2
Schemat3{ P1[ set , set ] } :
 for b being set ex a being set st P1[a,b]
provided
A1: ex a being set st
for b being set holds P1[a,b]
proofend;

scheme :: SCHEMS_1:sch 3
Schemat8{ P1[ set ], P2[ set ] } :
 ( ( for a being set holds P1[a] ) implies for a being set holds P2[a] )
provided
A1: for a being set st P1[a] holds
P2[a]
proofend;

scheme :: SCHEMS_1:sch 4
Schemat9{ P1[ set ], P2[ set ] } :
 ( ( for a being set holds P1[a] ) iff for a being set holds P2[a] )
provided
A1: for a being set holds
( P1[a] iff P2[a] )
proofend;

scheme :: SCHEMS_1:sch 5
Schemat17{ P1[ set ], P2[] } :
 ( ( for a being set holds P1[a] ) implies P2[] )
provided
A1: for a being set st P1[a] holds
P2[]
proofend;

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

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

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] )
proofend;

scheme :: SCHEMS_1:sch 9
Schemat22a{ P1[ set ], P2[ set ] } :
 for b being set ex a being set st
( P1[a] & P2[b] )
provided
A1: ( ex a being set st P1[a] & ( for b being set holds P2[b] ) )
proofend;

scheme :: SCHEMS_1:sch 10
Schemat22b{ P1[ set ], P2[ set ] } :
 ( ex a being set st P1[a] & ( for b being set holds P2[b] ) )
provided
A1: for b being set ex a being set st
( P1[a] & P2[b] )
proofend;

scheme :: SCHEMS_1:sch 11
Schemat23b{ P1[ set ], P2[ set ] } :
 ex a being set st
for b being set holds
( P1[a] & P2[b] )
provided
A1: for b being set ex a being set st
( P1[a] & P2[b] )
proofend;

scheme :: SCHEMS_1:sch 12
Schemat28{ P1[ set , set ] } :
 ex b being set st
for a being set holds P1[a,b]
provided
A1: for a, b being set holds P1[a,b]
proofend;

scheme :: SCHEMS_1:sch 13
Schemat30{ P1[ set , set ] } :
 ex a being set st P1[a,a]
provided
A1: ex a being set st
for b being set holds P1[a,b]
proofend;

scheme :: SCHEMS_1:sch 14
Schemat31{ P1[ set , set ] } :
 for a being set ex b being set st P1[b,a]
provided
A1: for a being set holds P1[a,a]
proofend;

scheme :: SCHEMS_1:sch 15
Schemat33{ P1[ set , set ] } :
 for a being set ex b being set st P1[a,b]
provided
A1: for a being set holds P1[a,a]
proofend;

scheme :: SCHEMS_1:sch 16
Schemat36{ P1[ set , set ] } :
 ex a, b being set st P1[a,b]
provided
A1: for b being set ex a being set st P1[a,b]
proofend;