set RR = the InternalRel of (PrecM R);
thus A0: PrecM R is asymmetric :: thesis:

let a, b be object ; :: according to RELAT_2:def 5,OPOSET_1:def 9 :: thesis:
assume ( a in the carrier of (PrecM R) & b in the carrier of (PrecM R) ) ; :: thesis:
then reconsider m = a, n = b as Element of (PrecM R) ;
assume ( [a,b] in the InternalRel of (PrecM R) & [b,a] in the InternalRel of (PrecM R) ) ; :: thesis:
then A0: ( m <= n & n <= m ) by ORDERS_2:def 5;
then ( m <> n & ( for x being Element of R holds
( not m . x > 0 or m . x < n . x or ex y being Element of R st
( n . y > 0 & x <= y ) ) ) & ( for x being Element of R holds
( not n . x > 0 or n . x < m . x or ex y being Element of R st
( m . y > 0 & x <= y ) ) ) ) by PM;
then consider x being Element of R such that
A2: m . x <> n . x by PBOOLE:def 21;
set X = { y where y is Element of R : ( m . y > 0 & x <= y ) } ;
ex y being Element of R st
( m . y > 0 & x <= y )

per cases by A2, XXREAL_0:1;

suppose m . x < n . x ; :: thesis:

hence ex y being Element of R st
( m . y > 0 & x <= y ) by A0, PM; :: thesis:

end;

suppose n . x < m . x ; :: thesis:

then consider y being Element of R such that
A5: ( n . y > 0 & x <= y ) by A0, PM;

per cases by A0, PM;

suppose n . y <= m . y ; :: thesis:

hence ex y being Element of R st
( m . y > 0 & x <= y ) by A5; :: thesis:

end;

suppose ex z being Element of R st
( m . z > 0 & y <= z ) ; :: thesis:

hence ex y being Element of R st
( m . y > 0 & x <= y ) by A5, ORDERS_2:3; :: thesis:

end;

then consider y being Element of R such that
A6: ( m . y > 0 & x <= y ) ;
A7: y in { y where y is Element of R : ( m . y > 0 & x <= y ) } by A6;
{ y where y is Element of R : ( m . y > 0 & x <= y ) } c= support m

proof

let z be object ; :: according to TARSKI:def 3 :: thesis:
assume z in { y where y is Element of R : ( m . y > 0 & x <= y ) } ; :: thesis:
then ex y being Element of R st
( z = y & m . y > 0 & x <= y ) ;
hence z in support m by PRE_POLY:def 7; :: thesis:

end;

then consider y being Element of R such that
A8: y is_maximal_in { y where y is Element of R : ( m . y > 0 & x <= y ) } by A7, Th12;
y in { y where y is Element of R : ( m . y > 0 & x <= y ) } by A8, WAYBEL_4:55;
then consider z being Element of R such that
A9: ( y = z & m . z > 0 & x <= z ) ;

per cases by A0, PM, A9;

suppose m . z < n . z ; :: thesis:

then consider u being Element of R such that
A10: ( m . u > 0 & z <= u ) by A0, PM;
x <= u by A9, A10, ORDERS_2:3;
then ( u in { y where y is Element of R : ( m . y > 0 & x <= y ) } & y < u ) by A9, A10, Lem2;
hence contradiction by A8, WAYBEL_4:55; :: thesis:

end;

suppose ex u being Element of R st
( n . u > 0 & z <= u ) ; :: thesis:

then consider u being Element of R such that
A11: ( n . u > 0 & z <= u ) ;

per cases by A0, PM;

suppose n . u <= m . u ; :: thesis:

then ( m . u > 0 & x <= u ) by A9, A11, ORDERS_2:3;
then ( u in { y where y is Element of R : ( m . y > 0 & x <= y ) } & y < u ) by A9, A11, Lem2;
hence contradiction by A8, WAYBEL_4:55; :: thesis:

end;

suppose ex v being Element of R st
( m . v > 0 & u <= v ) ; :: thesis:

then consider v being Element of R such that
A12: ( m . v > 0 & u <= v ) ;
A13: z <= v by A11, A12, ORDERS_2:3;
then x <= v by A9, ORDERS_2:3;
then ( v in { y where y is Element of R : ( m . y > 0 & x <= y ) } & y < v ) by A9, A12, A13, Lem2;
hence contradiction by A8, WAYBEL_4:55; :: thesis:

end;

thus PrecM R is transitive :: thesis:

proof

let a, b, c be object ; :: according to RELAT_2:def 8,ORDERS_2:def 3 :: thesis:
assume ( a in the carrier of (PrecM R) & b in the carrier of (PrecM R) & c in the carrier of (PrecM R) ) ; :: thesis:
assume A4: ( [a,b] in the InternalRel of (PrecM R) & [b,c] in the InternalRel of (PrecM R) ) ; :: thesis:
then reconsider a = a, b = b, c = c as Element of (PrecM R) by ZFMISC_1:87;
A6: ( a <= b & b <= c ) by A4, ORDERS_2:def 5;

A5: now :: thesis:

let x be Element of R; :: thesis:
assume a . x > 0 ; :: thesis:

per cases by A6, PM;

suppose A4: a . x < b . x ; :: thesis:

then ( b . x < c . x or ex y being Element of R st
( c . y > 0 & x <= y ) ) by A6, PM;
hence ( a . x < c . x or ex y being Element of R st
( c . y > 0 & x <= y ) ) by A4, XXREAL_0:2; :: thesis:

end;

suppose ex y being Element of R st
( b . y > 0 & x <= y ) ; :: thesis:

then consider y being Element of R such that
B1: ( b . y > 0 & x <= y ) ;

per cases by A6, PM;

suppose b . y <= c . y ; :: thesis:

hence ( a . x < c . x or ex y being Element of R st
( c . y > 0 & x <= y ) ) by B1; :: thesis:

end;

suppose ex z being Element of R st
( c . z > 0 & y <= z ) ; :: thesis:

then consider z being Element of R such that
B2: ( c . z > 0 & y <= z ) ;
thus ( a . x < c . x or ex y being Element of R st
( c . y > 0 & x <= y ) ) by B2, B1, ORDERS_2:3; :: thesis:

end;

a <> c by A4, A0, PREFER_1:22;
then a <= c by A5, PM;
hence [a,c] in the InternalRel of (PrecM R) by ORDERS_2:def 5; :: thesis:

end;