let B be set ; :: thesis: for C being Extension of B
for R being Rule
for E being Extension of R
for a being object st B,R |- a holds
C,E |- a
let C be Extension of B; :: thesis: for R being Rule
for E being Extension of R
for a being object st B,R |- a holds
C,E |- a
let R be Rule; :: thesis: for E being Extension of R
for a being object st B,R |- a holds
C,E |- a
let E be Extension of R; :: thesis: for a being object st B,R |- a holds
C,E |- a
let a be object ; :: thesis: ( B,R |- a implies C,E |- a )
( C is B -extending & E is R -extending ) ;
hence ( B,R |- a implies C,E |- a ) by Th44; :: thesis: verum