set Q = the InternalRel of (PrecPrecM R);
thus
PrecPrecM R is asymmetric
PrecPrecM R is transitive proof
let a,
b be
object ;
RELAT_2:def 5,
OPOSET_1:def 9 ( not a in the carrier of (PrecPrecM R) or not b in the carrier of (PrecPrecM R) or not [a,b] in the InternalRel of (PrecPrecM R) or not [b,a] in the InternalRel of (PrecPrecM R) )
assume
(
a in the
carrier of
(PrecPrecM R) &
b in the
carrier of
(PrecPrecM R) )
;
( not [a,b] in the InternalRel of (PrecPrecM R) or not [b,a] in the InternalRel of (PrecPrecM R) )
then reconsider m =
a,
n =
b as
Element of
(PrecPrecM R) ;
assume
(
[a,b] in the
InternalRel of
(PrecPrecM R) &
[b,a] in the
InternalRel of
(PrecPrecM R) )
;
contradiction
then
(
m <= n &
n <= m )
by ORDERS_2:def 5;
then
(
[(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the
carrier of
(PrecM R), the
InternalRel of
(PrecM R)) &
[(OrderedPartition n),(OrderedPartition m)] in LexOrder ( the
carrier of
(PrecM R), the
InternalRel of
(PrecM R)) )
by PPM;
hence
contradiction
by PREFER_1:22;
verum
end;
let a, b, c be object ; RELAT_2:def 8,ORDERS_2:def 3 ( not a in the carrier of (PrecPrecM R) or not b in the carrier of (PrecPrecM R) or not c in the carrier of (PrecPrecM R) or not [a,b] in the InternalRel of (PrecPrecM R) or not [b,c] in the InternalRel of (PrecPrecM R) or [a,c] in the InternalRel of (PrecPrecM R) )
assume
( a in the carrier of (PrecPrecM R) & b in the carrier of (PrecPrecM R) & c in the carrier of (PrecPrecM R) )
; ( not [a,b] in the InternalRel of (PrecPrecM R) or not [b,c] in the InternalRel of (PrecPrecM R) or [a,c] in the InternalRel of (PrecPrecM R) )
then reconsider m = a, n = b, o = c as Element of (PrecPrecM R) ;
assume
( [a,b] in the InternalRel of (PrecPrecM R) & [b,c] in the InternalRel of (PrecPrecM R) )
; [a,c] in the InternalRel of (PrecPrecM R)
then
( m <= n & n <= o )
by ORDERS_2:def 5;
then
( [(OrderedPartition m),(OrderedPartition n)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) & [(OrderedPartition n),(OrderedPartition o)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R)) )
by PPM;
then
[(OrderedPartition m),(OrderedPartition o)] in LexOrder ( the carrier of (PrecM R), the InternalRel of (PrecM R))
by RELAT_2:31;
then
m <= o
by PPM;
hence
[a,c] in the InternalRel of (PrecPrecM R)
by ORDERS_2:def 5; verum