schems_1.miz

    begin

    reserve a,b,d for set;

    scheme :: SCHEMS_1:sch1

    Schemat0 { P[ set] } :

ex a st P[a]

      provided

       A1: for a holds P[a];

      set a = the set;

      P[a] by A1;

      hence thesis;

    end;

    scheme :: SCHEMS_1:sch2

    Schemat3 { S[ set, set] } :

for b holds ex a st S[a, b]

      provided

       A1: ex a st for b holds S[a, b];

      thus thesis by A1;

    end;

    scheme :: SCHEMS_1:sch3

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

      thus thesis by A1;

    end;

    scheme :: SCHEMS_1:sch4

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

      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 :: SCHEMS_1:sch5

    Schemat17 { P[ set], T[] } :

(for a holds P[a]) implies T[]

      provided

       A1: for a holds P[a] implies T[];

      assume

       A2: for a holds P[a];

      now

        let a;

        P[a] by A2;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    scheme :: SCHEMS_1:sch6

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

      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 :: SCHEMS_1:sch7

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

      thus thesis by A1;

    end;

    scheme :: SCHEMS_1:sch8

    Schemat20b { P[ set], Q[ set] } :

ex a st for b holds P[a] or Q[b]

      provided

       A1: for b holds ex a st P[a] or Q[b];



       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 :: SCHEMS_1:sch9

    Schemat22a { P[ set], Q[ set] } :

for b holds ex a st P[a] & Q[b]

      provided

       A1: (ex a st P[a]) & for b holds Q[b];

      thus thesis by A1;

    end;

    scheme :: SCHEMS_1:sch10

    Schemat22b { P[ set], Q[ set] } :

(ex a st P[a]) & for b holds Q[b]

      provided

       A1: for b holds ex a st P[a] & Q[b];

      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 :: SCHEMS_1:sch11

    Schemat23b { P[ set], Q[ set] } :

ex a st for b holds P[a] & Q[b]

      provided

       A1: for b holds ex a st P[a] & Q[b];



       A2: for b holds 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 :: SCHEMS_1:sch12

    Schemat28 { S[ set, set] } :

ex b st for a holds S[a, b]

      provided

       A1: for a, b holds S[a, b];

      now

        let b;

        for a holds S[a, b] by A1;

        hence thesis;

      end;

      hence thesis;

    end;

    scheme :: SCHEMS_1:sch13

    Schemat30 { S[ set, set] } :

ex a st S[a, a]

      provided

       A1: ex a st for b holds S[a, b];

      thus thesis by A1;

    end;

    scheme :: SCHEMS_1:sch14

    Schemat31 { S[ set, set] } :

for a holds ex b st S[b, a]

      provided

       A1: for a holds S[a, a];

      thus thesis by A1;

    end;

    scheme :: SCHEMS_1:sch15

    Schemat33 { S[ set, set] } :

for a holds ex b st S[a, b]

      provided

       A1: for a holds S[a, a];

      thus thesis by A1;

    end;

    scheme :: SCHEMS_1:sch16

    Schemat36 { S[ set, set] } :

ex a, b st S[a, b]

      provided

       A1: for b holds ex a st S[a, b];

      set b = the set;

      ex a st S[a, b] by A1;

      hence thesis;

    end;