thus ( a is B,R -provable implies for C being Extension of B
for E being Extension of R holds C,E |- a ) by Th54; :: thesis: ( ( for C being Extension of B
for E being Extension of R holds C,E |- a ) implies a is B,R -provable )
assume A10: for C being Extension of B
for E being Extension of R holds C,E |- a ; :: thesis: a is B,R -provable
( B is B -extending & R is R -extending ) ;
hence a is B,R -provable by A10; :: thesis: verum