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 ;

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

hence
G |-0 A
by A1; :: thesis: verumprc0 f,G,i

let i be Nat; :: thesis: ( 1 <= i & i <= len f implies prc0 f,G,b_{1} )

assume ( 1 <= i & i <= len f ) ; :: thesis: prc0 f,G,b_{1}

end;assume ( 1 <= i & i <= len f ) ; :: thesis: prc0 f,G,b

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 Def29, A2;

end;

( 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 Def29, A2;

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,b_{1}

end;

( 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,b

end;