let p be Element of PL-WFF ; :: thesis: for F being Subset of PL-WFF st ( p in PL_axioms or p in F ) holds
F |- p
let F be Subset of PL-WFF; :: thesis: ( ( p in PL_axioms or p in F ) implies F |- p )
defpred S₁[ set , set ] means $2 = p;
A1: for k being Nat st k in Seg 1 holds
ex x being Element of PL-WFF st S₁[k,x] ;
consider f being FinSequence of PL-WFF such that
A2: ( dom f = Seg 1 & ( for k being Nat st k in Seg 1 holds
S₁[k,f . k] ) ) from FINSEQ_1:sch 5(A1);
A3: len f = 1 by A2, FINSEQ_1:def 3;
1 in Seg 1 ;
then A4: f . 1 = p by A2;
assume A5: ( p in PL_axioms or p in F ) ; :: thesis: F |- p
for j being Nat st 1 <= j & j <= len f holds
prc f,F,j

proof

let j be Nat; :: thesis: ( 1 <= j & j <= len f implies prc f,F,j )
assume A6: ( 1 <= j & j <= len f ) ; :: thesis: prc f,F,j

per cases ( p in PL_axioms or p in F ) by A5;

suppose p in PL_axioms ; :: thesis: prc f,F,j

hence prc f,F,j by A3, A4, A6, XXREAL_0:1; :: thesis: verum

end;

suppose p in F ; :: thesis: prc f,F,j

hence prc f,F,j by A3, A4, A6, XXREAL_0:1; :: thesis: verum

end;

end;

end;

hence F |- p by A3, A4; :: thesis: verum