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

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