let UN be Universe; :: thesis: for R being Relation st dom R is Element of UN & rng R is Element of UN holds
R is Element of UN
let R be Relation; :: thesis: ( dom R is Element of UN & rng R is Element of UN implies R is Element of UN )
assume that
A1: dom R is Element of UN and
A2: rng R is Element of UN ; :: thesis: R is Element of UN
A3: R c= [:(dom R),(rng R):] by RELAT_1:7;
[:(dom R),(rng R):] is Element of UN by A1, A2, CLASSES2:61;
hence R is Element of UN by A3, Th13; :: thesis: verum