let R, S be RelStr ; ( 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 )
; 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 ;
RELAT_2:def 4 ( 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)
;
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 A13:
(
x in the
carrier of
R &
y in the
carrier of
S )
;
x = ythen 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;
verum end; suppose A15:
(
x in the
carrier of
S &
y in the
carrier of
R )
;
x = ythen 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;
verum end;
end;
hence
R [*] S is antisymmetric
by ORDERS_2:def 4; verum