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 ( X in U & Y in U ) ; :: thesis: for R being Relation of X,Y holds R in U
then [:X,Y:] in U by CLASSES2:67;
hence for R being Relation of X,Y holds R in U by CLASSES1:def 1; :: thesis: verum