let B1 be set ; :: thesis: ( B1 is C -extending implies B1 is B -extending )
A1: C is B -extending ;
assume B1 is C -extending ; :: thesis: B1 is B -extending
hence B1 is B -extending by A1, XBOOLE_1:1; :: thesis: verum