let A be Element of LTLB_WFF ; :: thesis: for F, G being Subset of LTLB_WFF st F c= G & F |- A holds
G |- A
let F, G be Subset of LTLB_WFF; :: thesis: ( F c= G & F |- A implies G |- A )
assume A0: ( F c= G & F |- A ) ; :: thesis: G |- A
then consider f being FinSequence of LTLB_WFF such that
A1: ( f . (len f) = A & 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,G,i

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies prc f,G,b₁ )
assume ( 1 <= i & i <= len f ) ; :: thesis: prc f,G,b₁

per cases then ( f . i in F or f . i in LTL_axioms 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 LTLAXIO1:def 29, A2;

suppose f . i in F ; :: thesis: prc f,G,b₁

hence prc f,G,i by A0; :: thesis: verum

end;

suppose ( f . i in LTL_axioms 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 ) ) ; :: thesis: prc f,G,b₁

hence prc f,G,i ; :: thesis: verum

end;

end;

end;

hence G |- A by A1; :: thesis: verum