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 ;

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

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

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

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

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