:: Schemes :: by Stanis\l aw T. Czuba :: :: Received December 17, 1990 :: Copyright (c) 1990-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ begin reserve a,b,d for set; scheme :: SCHEMS_1:sch 1 Schemat0 {P[set]} : ex a st P[a] provided for a holds P[a]; scheme :: SCHEMS_1:sch 2 Schemat3 {S[set,set]} : for b ex a st S[a,b] provided ex a st for b holds S[a,b]; scheme :: SCHEMS_1:sch 3 Schemat8 {P[set],Q[set]} : (for a holds P[a]) implies for a holds Q[a] provided for a holds P[a] implies Q[a]; scheme :: SCHEMS_1:sch 4 Schemat9 {P[set],Q[set]} : (for a holds P[a]) iff for a holds Q[a] provided for a holds P[a] iff Q[a]; scheme :: SCHEMS_1:sch 5 Schemat17 {P[set],T[]} : (for a holds P[a]) implies T[] provided for a holds P[a] implies T[]; scheme :: SCHEMS_1:sch 6 Schemat18a {P[set],Q[set]} : ex a st for b holds P[a] or Q[b] provided (ex a st P[a]) or for b holds Q[b]; scheme :: SCHEMS_1:sch 7 Schemat18b {P[set],Q[set]} : (ex a st P[a]) or for b holds Q[b] provided ex a st for b holds P[a] or Q[b]; scheme :: SCHEMS_1:sch 8 Schemat20b {P[set],Q[set]} : ex a st for b holds P[a] or Q[b] provided for b ex a st P[a] or Q[b]; scheme :: SCHEMS_1:sch 9 Schemat22a {P[set],Q[set]} : for b ex a st P[a] & Q[b] provided (ex a st P[a]) & for b holds Q[b]; scheme :: SCHEMS_1:sch 10 Schemat22b {P[set],Q[set]} : (ex a st P[a]) & for b holds Q[b] provided for b ex a st P[a] & Q[b]; scheme :: SCHEMS_1:sch 11 Schemat23b {P[set],Q[set]} : ex a st for b holds P[a] & Q[b] provided for b ex a st P[a] & Q[b]; scheme :: SCHEMS_1:sch 12 Schemat28 {S[set,set]} : ex b st for a holds S[a,b] provided for a,b holds S[a,b]; scheme :: SCHEMS_1:sch 13 Schemat30 {S[set,set]} : ex a st S[a,a] provided ex a st for b holds S[a,b]; scheme :: SCHEMS_1:sch 14 Schemat31 {S[set,set]} : for a ex b st S[b,a] provided for a holds S[a,a]; scheme :: SCHEMS_1:sch 15 Schemat33 {S[set,set]} : for a ex b st S[a,b] provided for a holds S[a,a]; scheme :: SCHEMS_1:sch 16 Schemat36 {S[set,set]} : ex a,b st S[a,b] provided for b ex a st S[a,b];