let A be Element of LTLB_WFF ; :: thesis:
let F, G be Subset of LTLB_WFF; :: thesis:
assume A0: ( F c= G & F |-0 A ) ; :: thesis:
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 ;

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:

end;