let X, Y be non empty reflexive RelStr ; :: thesis: ( [:X,Y:] is antisymmetric implies ( X is antisymmetric & Y is antisymmetric ) )
assume A1: [:X,Y:] is antisymmetric ; :: thesis: ( X is antisymmetric & Y is antisymmetric )
for x, y being Element of X st x <= y & y <= x holds
x = y

proof

consider z being Element of Y;
A2: z <= z ;
let x, y be Element of X; :: thesis: ( x <= y & y <= x implies x = y )
assume ( x <= y & y <= x ) ; :: thesis: x = y
then ( [x,z] <= [y,z] & [y,z] <= [x,z] ) by A2, Th11;
then [x,z] = [y,z] by A1, YELLOW_0:def 3;
hence x = y by ZFMISC_1:33; :: thesis: verum

end;

hence X is antisymmetric by YELLOW_0:def 3; :: thesis: Y is antisymmetric
for x, y being Element of Y st x <= y & y <= x holds
x = y

proof

consider z being Element of X;
A3: z <= z ;
let x, y be Element of Y; :: thesis: ( x <= y & y <= x implies x = y )
assume ( x <= y & y <= x ) ; :: thesis: x = y
then ( [z,x] <= [z,y] & [z,y] <= [z,x] ) by A3, Th11;
then [z,x] = [z,y] by A1, YELLOW_0:def 3;
hence x = y by ZFMISC_1:33; :: thesis: verum

end;

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