:: Schemes :: by Stanis\l aw T. Czuba :: :: Received December 17, 1990 :: Copyright (c) 1990-2018 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 Schemat0 {P[set]} : ex a st P[a] provided A1: for a holds P[a] proof set a = the set; P[a] by A1; hence thesis; end; scheme Schemat3 {S[set,set]} : for b ex a st S[a,b] provided A1: ex a st for b holds S[a,b] proof thus thesis by A1; end; scheme Schemat8 {P[set],Q[set]} : (for a holds P[a]) implies for a holds Q[a] provided A1: for a holds P[a] implies Q[a] proof thus thesis by A1; end; scheme Schemat9 {P[set],Q[set]} : (for a holds P[a]) iff for a holds Q[a] provided A1: for a holds P[a] iff Q[a] proof thus (for a holds P[a]) implies for a holds Q[a] by A1; assume A2: for a holds Q[a]; for a holds P[a] by A1,A2; hence thesis; end; scheme Schemat17 {P[set],T[]} : (for a holds P[a]) implies T[] provided A1: for a holds P[a] implies T[] proof assume A2: for a holds P[a]; now let a; P[a] by A2; hence thesis by A1; end; hence thesis; end; scheme Schemat18a {P[set],Q[set]} : ex a st for b holds P[a] or Q[b] provided A1: (ex a st P[a]) or for b holds Q[b] proof now A2: now set a = the set; assume for b holds Q[b]; then for b holds P[a] or Q[b]; hence thesis; end; now given a such that A3: P[a]; for b holds P[a] or Q[b] by A3; hence thesis; end; hence thesis by A1,A2; end; hence thesis; end; scheme Schemat18b {P[set],Q[set]} : (ex a st P[a]) or for b holds Q[b] provided A1: ex a st for b holds P[a] or Q[b] proof thus thesis by A1; end; scheme Schemat20b {P[set],Q[set]} : ex a st for b holds P[a] or Q[b] provided A1: for b ex a st P[a] or Q[b] proof A2: (ex a st P[a]) or for b holds Q[b] by A1; ex a st for b holds P[a] or Q[b] from Schemat18a(A2); hence thesis; end; scheme Schemat22a {P[set],Q[set]} : for b ex a st P[a] & Q[b] provided A1: (ex a st P[a]) & for b holds Q[b] proof thus thesis by A1; end; scheme Schemat22b {P[set],Q[set]} : (ex a st P[a]) & for b holds Q[b] provided A1: for b ex a st P[a] & Q[b] proof assume A2: (for a holds not P[a]) or ex b st not Q[b]; per cases by A2; suppose ex b st not Q[b]; then consider b such that A3: not Q[b]; now let d; assume d = b; ex a st P[a] & Q[b] by A1; hence contradiction by A3; end; hence thesis; end; suppose A4: for a holds not P[a]; now let b; ex a st ( P[a])& Q[b] by A1; hence thesis by A4; end; hence thesis; end; end; scheme Schemat23b {P[set],Q[set]} : ex a st for b holds P[a] & Q[b] provided A1: for b ex a st P[a] & Q[b] proof A2: for b ex a st P[a] & Q[b] by A1; (ex a st P[a]) & for b holds Q[b] from Schemat22b(A2); hence thesis; end; scheme Schemat28 {S[set,set]} : ex b st for a holds S[a,b] provided A1: for a,b holds S[a,b] proof now let b; for a holds S[a,b] by A1; hence thesis; end; hence thesis; end; scheme Schemat30 {S[set,set]} : ex a st S[a,a] provided A1: ex a st for b holds S[a,b] proof thus thesis by A1; end; scheme Schemat31 {S[set,set]} : for a ex b st S[b,a] provided A1: for a holds S[a,a] proof thus thesis by A1; end; scheme Schemat33 {S[set,set]} : for a ex b st S[a,b] provided A1: for a holds S[a,a] proof thus thesis by A1; end; scheme Schemat36 {S[set,set]} : ex a,b st S[a,b] provided A1: for b ex a st S[a,b] proof set b = the set; ex a st S[a,b] by A1; hence thesis; end;