set Q = the InternalRel of (PrecPrecM R);
thus PrecPrecM R is asymmetric :: thesis: PrecPrecM R is transitive

proof

let a, b be object ; :: according to RELAT_2:def 5,OPOSET_1:def 9 :: thesis: ( 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) ) ; :: thesis: ( 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) ) ; :: thesis: 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; :: thesis: verum

end;

let a, b, c be object ; :: according to RELAT_2:def 8,ORDERS_2:def 3 :: thesis: ( 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) ) ; :: thesis: ( 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) ) ; :: thesis: [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; :: thesis: verum