let p, q be Element of LTLB_WFF ; :: thesis: for F being Subset of LTLB_WFF st F |- q holds
F \/ {p} |- q
let F be Subset of LTLB_WFF; :: thesis: ( F |- q implies F \/ {p} |- q )
assume F |- q ; :: thesis: 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 :: thesis: for i being Nat st 1 <= i & i <= len f holds
prc f,F \/ {p},i
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies prc f,F \/ {p},i )
assume ( 1 <= i & i <= len f ) ; :: thesis: prc f,F \/ {p},i
then ( 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 ; :: thesis: verum
end;
hence F \/ {p} |- q by A1; :: thesis: verum