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