set IT = Y |^ X;

now :: thesis: for x, y being Element of (Y |^ X) st x <= y & y <= x holds
x = y

let x, y be Element of (Y |^ X); :: thesis: ( x <= y & y <= x implies x = y )
reconsider x19 = x, y19 = y as Function of X, the carrier of Y by Lm5;
reconsider x1 = x, y1 = y as Element of (product (X --> Y)) ;
assume that
A1: x <= y and
A2: y <= x ; :: thesis: x = y
y1 in the carrier of (product (X --> Y)) ;
then y1 in product (Carrier (X --> Y)) by Def4;
then consider f1, g1 being Function such that
A3: ( f1 = y1 & g1 = x1 ) and
A4: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f1 . i & yi = g1 . i & xi <= yi ) by A2, Def4;
x1 in the carrier of (product (X --> Y)) ;
then x1 in product (Carrier (X --> Y)) by Def4;
then consider f, g being Function such that
A5: ( f = x1 & g = y1 ) and
A6: for i being object st i in X holds
ex R being RelStr ex xi, yi being Element of R st
( R = (X --> Y) . i & xi = f . i & yi = g . i & xi <= yi ) by A1, Def4;

A7: now :: thesis: for i being object st i in X holds
x19 . i = y19 . i

let i be object ; :: thesis: ( i in X implies x19 . i = y19 . i )
assume A8: i in X ; :: thesis: x19 . i = y19 . i
then consider R2 being RelStr , xi2, yi2 being Element of R2 such that
A9: R2 = (X --> Y) . i and
A10: ( xi2 = f1 . i & yi2 = g1 . i & xi2 <= yi2 ) by A4;
A11: Y = R2 by A8, A9, FUNCOP_1:7;
consider R1 being RelStr , xi1, yi1 being Element of R1 such that
A12: R1 = (X --> Y) . i and
A13: ( xi1 = f . i & yi1 = g . i & xi1 <= yi1 ) by A6, A8;
Y = R1 by A8, A12, FUNCOP_1:7;
hence x19 . i = y19 . i by A5, A3, A13, A10, A11, ORDERS_2:2; :: thesis: verum

end;

( dom x19 = X & dom y19 = X ) by FUNCT_2:def 1;
hence x = y by A7, FUNCT_1:2; :: thesis: verum

end;

hence Y |^ X is antisymmetric by YELLOW_0:def 3; :: thesis: verum