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_{1}[ 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_{1}[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_{1}[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

X |- p

let X be Subset of LTLB_WFF; :: thesis: ( ( p in LTL_axioms or p in X ) implies X |- p )

defpred S

A1: for k being Nat st k in Seg 1 holds

ex x being Element of LTLB_WFF st S

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

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

hence
X |- p
by A3, A4; :: thesis: verum
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

end;assume A6: ( 1 <= j & j <= len g ) ; :: thesis: prc g,X,j

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

end;