let X, Y be set ; :: thesis: for R being Relation st R c= [:X,Y:] holds
( dom R c= X & rng R c= Y )
let R be Relation; :: thesis: ( R c= [:X,Y:] implies ( dom R c= X & rng R c= Y ) )
assume R c= [:X,Y:] ; :: thesis: ( dom R c= X & rng R c= Y )
then R /\ [:X,Y:] = R by XBOOLE_1:28;
hence ( dom R c= X & rng R c= Y ) by Th1; :: thesis: verum