let R1 be Rule; :: thesis: ( R1 is E -extending implies R1 is R -extending )
A1: E is R -extending ;
assume R1 is E -extending ; :: thesis: R1 is R -extending
hence R1 is R -extending by A1, XBOOLE_1:1; :: thesis: verum