let U be Universe; :: thesis: for X, Y being set st X in U & Y in U holds
for R being Relation of X,Y holds R in U
let X, Y be set ; :: thesis: ( X in U & Y in U implies for R being Relation of X,Y holds R in U )
assume that
A1: X in U and
A2: Y in U ; :: thesis: for R being Relation of X,Y holds R in U
[:X,Y:] in U by A1, A2, CLASSES2:61;
hence for R being Relation of X,Y holds R in U by CLASSES1:def 1; :: thesis: verum