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

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

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

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 ;

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

hence
F |-0 A
by A3, A4; :: thesis: verum
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

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

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

end;