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 ;

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

hence
F \/ {p} |- q
by A1; :: thesis: verumprc 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;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