let p, q be Element of LTLB_WFF ; for F being Subset of LTLB_WFF st F |- q holds
F \/ {p} |- q
let F be Subset of LTLB_WFF; ( F |- q implies F \/ {p} |- q )
assume
F |- q
; F \/ {p} |- q
then consider f being FinSequence of LTLB_WFF such that
A1:
( f . (len f) = q & 1 <= len f )
and
A2:
for i being Nat st 1 <= i & i <= len f holds
prc f,F,i
;
now for i being Nat st 1 <= i & i <= len f holds
prc f,F \/ {p},ilet i be
Nat;
( 1 <= i & i <= len f implies prc f,F \/ {p},i )assume
( 1
<= i &
i <= len f )
;
prc f,F \/ {p},ithen
(
f . i in LTL_axioms or
f . i in F or ex
j,
k being
Nat st
( ( 1
<= j &
j < i & 1
<= k &
k < i & (
f /. j,
f /. k MP_rule f /. i or
f /. j,
f /. k IND_rule f /. i ) ) or ex
j being
Nat st
( 1
<= j &
j < i &
f /. j NEX_rule f /. i ) ) )
by Def29, A2;
then
(
f . i in LTL_axioms or
f . i in F \/ {p} or ex
j,
k being
Nat st
( ( 1
<= j &
j < i & 1
<= k &
k < i & (
f /. j,
f /. k MP_rule f /. i or
f /. j,
f /. k IND_rule f /. i ) ) or ex
j being
Nat st
( 1
<= j &
j < i &
f /. j NEX_rule f /. i ) ) )
by XBOOLE_0:def 3;
hence
prc f,
F \/ {p},
i
;
verum end;
hence
F \/ {p} |- q
by A1; verum