let R, S be RelStr ; :: thesis: ( R tolerates S & the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R is transitive & R is antisymmetric & S is transitive & S is antisymmetric implies R [*] S is antisymmetric )
set X = the carrier of (R [*] S);
set F = the InternalRel of (R [*] S);
assume A1: ( R tolerates S & the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R is transitive & R is antisymmetric & S is transitive & S is antisymmetric ) ; :: thesis: R [*] S is antisymmetric
then A2: ( the InternalRel of R is_antisymmetric_in the carrier of R & the InternalRel of S is_antisymmetric_in the carrier of S ) by ORDERS_2:def 6;
the InternalRel of (R [*] S) is_antisymmetric_in the carrier of (R [*] S)

proof

let x, y be set ; :: according to RELAT_2:def 4 :: thesis: ( not x in the carrier of (R [*] S) or not y in the carrier of (R [*] S) or not [x,y] in the InternalRel of (R [*] S) or not [y,x] in the InternalRel of (R [*] S) or x = y )
assume A3: ( x in the carrier of (R [*] S) & y in the carrier of (R [*] S) & [x,y] in the InternalRel of (R [*] S) & [y,x] in the InternalRel of (R [*] S) ) ; :: thesis: x = y
then A4: x in the carrier of R \/ the carrier of S by Def2;
A5: y in the carrier of R \/ the carrier of S by A3, Def2;

per cases ( ( x in the carrier of R & y in the carrier of R ) or ( x in the carrier of R & y in the carrier of S ) or ( x in the carrier of S & y in the carrier of R ) or ( x in the carrier of S & y in the carrier of S ) ) by A4, A5, XBOOLE_0:def 3;

suppose A6: ( x in the carrier of R & y in the carrier of R ) ; :: thesis: x = y

then ( [x,y] in the InternalRel of R & [y,x] in the InternalRel of R ) by A1, A3, Th4;
hence x = y by A2, A6, RELAT_2:def 4; :: thesis: verum

end;

suppose A7: ( x in the carrier of R & y in the carrier of S ) ; :: thesis: x = y

then A8: y in the carrier of R by A1, A3, Th21;
then ( [x,y] in the InternalRel of R & [y,x] in the InternalRel of R ) by A1, A3, A7, Th4;
hence x = y by A2, A7, A8, RELAT_2:def 4; :: thesis: verum

end;

suppose A9: ( x in the carrier of S & y in the carrier of R ) ; :: thesis: x = y

then A10: y in the carrier of S by A1, A3, Th17;
then ( [x,y] in the InternalRel of S & [y,x] in the InternalRel of S ) by A1, A3, A9, Th5;
hence x = y by A2, A9, A10, RELAT_2:def 4; :: thesis: verum

end;

suppose A11: ( x in the carrier of S & y in the carrier of S ) ; :: thesis: x = y

then ( [x,y] in the InternalRel of S & [y,x] in the InternalRel of S ) by A1, A3, Th5;
hence x = y by A2, A11, RELAT_2:def 4; :: thesis: verum

end;

end;

end;

hence R [*] S is antisymmetric by ORDERS_2:def 6; :: thesis: verum