let a be object ; :: thesis: ( not a is C -axiomatic implies not a is B -axiomatic )
assume A1: not a in C ; :: according to PROOFS_1:def 9 :: thesis: not a is B -axiomatic
C is B -extending ;
hence not a in B by A1; :: according to PROOFS_1:def 9 :: thesis: verum