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

proof

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

per cases ( A in LTL0_axioms or A in F ) by A5;

suppose A in LTL0_axioms ; :: thesis: prc0 g,F,j

hence prc0 g,F,j by A3, A4, A6, XXREAL_0:1; :: thesis: verum

end;

suppose A in F ; :: thesis: prc0 g,F,j

hence prc0 g,F,j by A3, A4, A6, XXREAL_0:1; :: thesis: verum

end;

end;

end;

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