let X be set ; :: thesis: for S being Relation
for R being X -defined Relation st R c= S holds
R c= S | X
let S be Relation; :: thesis: for R being X -defined Relation st R c= S holds
R c= S | X
let R be X -defined Relation; :: thesis: ( R c= S implies R c= S | X )
R = R | X ;
hence ( R c= S implies R c= S | X ) by Th70; :: thesis: verum