let UN be Universe; :: thesis: for R being Relation st R in UN holds
( dom R in UN & rng R in UN )
let R be Relation; :: thesis: ( R in UN implies ( dom R in UN & rng R in UN ) )
assume R in UN ; :: thesis: ( dom R in UN & rng R in UN )
then ( dom R is Element of UN & rng R is Element of UN ) by Th36;
hence ( dom R in UN & rng R in UN ) ; :: thesis: verum