let X, Y be set ; :: thesis: for f being Function holds <:f,X,Y:> c= f
let f be Function; :: thesis: <:f,X,Y:> c= f
( <:f,X,Y:> = (Y | f) | X & (Y | f) | X c= Y | f & Y | f c= f ) by RELAT_1:88, RELAT_1:117;
hence <:f,X,Y:> c= f by XBOOLE_1:1; :: thesis: verum