let G2 be ESubgraph of G; :: thesis: G2 is real-elabeled
the_ELabel_of G2 = (the_ELabel_of G) | (the_Edges_of G2) by Def11;
hence G2 is real-elabeled ; :: thesis: verum