let A be Element of LTLB_WFF ; :: thesis: for F, G being Subset of LTLB_WFF st F c= G & F |-0 A holds
G |-0 A

let F, G be Subset of LTLB_WFF; :: thesis: ( F c= G & F |-0 A implies G |-0 A )
assume A0: ( F c= G & F |-0 A ) ; :: thesis: G |-0 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
prc0 f,F,i ;
now :: thesis: for i being Nat st 1 <= i & i <= len f holds
prc0 f,G,i
let i be Nat; :: thesis: ( 1 <= i & i <= len f implies prc0 f,G,b1 )
assume ( 1 <= i & i <= len f ) ; :: thesis: prc0 f,G,b1
per cases then ( f . i in F or f . i in LTL0_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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) )
by ;
suppose f . i in F ; :: thesis: prc0 f,G,b1
hence prc0 f,G,i by A0; :: thesis: verum
end;
suppose ( f . i in LTL0_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 MP0_rule f /. i or f /. j,f /. k IND0_rule f /. i ) ) or ex j being Nat st
( 1 <= j & j < i & ( f /. j NEX0_rule f /. i or f /. j REFL0_rule f /. i ) ) ) ; :: thesis: prc0 f,G,b1
hence prc0 f,G,i ; :: thesis: verum
end;
end;
end;
hence G |-0 A by A1; :: thesis: verum