defpred S₁[ Element of MP-WFF ] means ( $1 = VERUM or $1 is atomic MP-wff or $1 is negative MP-wff or $1 is necessitive MP-wff or $1 is conjunctive MP-wff );
A1: S₁[ VERUM ] ;
A2: for A being Element of MP-WFF st S₁[A] holds
S₁[ 'not' A] by Def17;
A3: for A, B being Element of MP-WFF st S₁[A] & S₁[B] holds
S₁[A '&' B] by Def19;
A4: for A being Element of MP-WFF st S₁[A] holds
S₁[ (#) A] by Def18;
A5: for p being MP-variable holds S₁[ @ p] by Def16;
thus for A being Element of MP-WFF holds S₁[A] from MODAL_1:sch 1(A1, A5, A2, A4, A3); :: thesis: verum