let p be Element of LTLB_WFF ; :: thesis: for X being Subset of LTLB_WFF st ( p in LTL_axioms or p in X ) holds
X |- p
let X be Subset of LTLB_WFF; :: thesis: ( ( p in LTL_axioms or p in X ) implies X |- p )
defpred S₁[ set , set ] means $2 = p;
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 by FINSEQ_1:2, TARSKI:def 1;
then A4: g . 1 = p by A2;
assume A5: ( p in LTL_axioms or p in X ) ; :: thesis: X |- p
for j being Nat st 1 <= j & j <= len g holds
prc g,X,j

proof

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

per cases ( p in LTL_axioms or p in X ) by A5;

suppose p in LTL_axioms ; :: thesis: prc g,X,j

then g . j in LTL_axioms by A3, A4, A6, XXREAL_0:1;
hence prc g,X,j ; :: thesis: verum

end;

suppose p in X ; :: thesis: prc g,X,j

then g . j in X by A3, A4, A6, XXREAL_0:1;
hence prc g,X,j ; :: thesis: verum

end;

end;

end;

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