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 that
A1: R tolerates S and
A2: the carrier of R /\ the carrier of S is upper Subset of R and
A3: the carrier of R /\ the carrier of S is lower Subset of S and
A4: ( R is transitive & R is antisymmetric ) and
A5: ( S is transitive & S is antisymmetric ) ; :: thesis: R [*] S is antisymmetric
A6: the InternalRel of S is_antisymmetric_in the carrier of S by A5, ORDERS_2:def 4;
A7: the InternalRel of R is_antisymmetric_in the carrier of R by A4, ORDERS_2:def 4;
the InternalRel of (R [*] S) is_antisymmetric_in the carrier of (R [*] S)

proof

let x, y be object ; :: 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 that
A8: ( x in the carrier of (R [*] S) & y in the carrier of (R [*] S) ) and
A9: [x,y] in the InternalRel of (R [*] S) and
A10: [y,x] in the InternalRel of (R [*] S) ; :: thesis: x = y
A11: ( x in the carrier of R \/ the carrier of S & y in the carrier of R \/ the carrier of S ) by A8, 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 A11, XBOOLE_0:def 3;

suppose A12: ( 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, A4, A9, A10, Th4;
hence x = y by A7, A12; :: thesis: verum

end;

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

then A14: y in the carrier of R by A3, A10, Th21;
then ( [x,y] in the InternalRel of R & [y,x] in the InternalRel of R ) by A1, A4, A9, A10, A13, Th4;
hence x = y by A7, A13, A14; :: thesis: verum

end;

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

then A16: y in the carrier of S by A2, A9, Th17;
then ( [x,y] in the InternalRel of S & [y,x] in the InternalRel of S ) by A1, A5, A9, A10, A15, Th5;
hence x = y by A6, A15, A16; :: thesis: verum

end;

suppose A17: ( 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, A5, A9, A10, Th5;
hence x = y by A6, A17; :: thesis: verum

end;

end;

end;

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