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 )
dom R c= X by Def18;
then A: R = R | X by Th97;
assume R c= S ; :: thesis: R c= S | X
hence R c= S | X by A, Th105; :: thesis: verum