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
set z = the Element of Y;
A2: the Element of Y <= the Element of Y ;
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, the Element of Y] <= [y, the Element of Y] & [y, the Element of Y] <= [x, the Element of Y] ) by A2, Th11;
then [x, the Element of Y] = [y, the Element of Y] by A1, YELLOW_0:def 3;
hence x = y by XTUPLE_0:1; :: 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
set z = the Element of X;
A3: the Element of X <= the Element of X ;
let x, y be Element of Y; :: thesis: ( x <= y & y <= x implies x = y )
assume ( x <= y & y <= x ) ; :: thesis: x = y
then ( [ the Element of X,x] <= [ the Element of X,y] & [ the Element of X,y] <= [ the Element of X,x] ) by A3, Th11;
then [ the Element of X,x] = [ the Element of X,y] by A1, YELLOW_0:def 3;
hence x = y by XTUPLE_0:1; :: thesis: verum
end;
hence Y is antisymmetric by YELLOW_0:def 3; :: thesis: verum