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 S1[ set , set ] means $2 = p;
A1: for k being Nat st k in Seg 1 holds
ex x being Element of PL-WFF st S1[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
S1[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 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