thus ( R is serial implies for x being Element of R ex y being Element of R st x <= y ) :: thesis: ( ( for x being Element of R ex y being Element of R st x <= y ) implies R is serial )

proof

assume A1: R is serial ; :: thesis: for x being Element of R ex y being Element of R st x <= y
set IR = the InternalRel of R;
set X = the carrier of R;
let x be Element of R; :: thesis: ex y being Element of R st x <= y
consider y being object such that
A2: ( y in the carrier of R & [x,y] in the InternalRel of R ) by Def1, A1;
thus ex y being Element of R st x <= y by A2, ORDERS_2:def 5; :: thesis: verum

end;

assume A3: for x being Element of R ex y being Element of R st x <= y ; :: thesis: R is serial
the InternalRel of R is_serial_in the carrier of R

proof

let x be object ; :: according to ROUGHS_2:def 1 :: thesis: ( x in the carrier of R implies ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R ) )
assume x in the carrier of R ; :: thesis: ex y being object st
( y in the carrier of R & [x,y] in the InternalRel of R )
then reconsider xx = x as Element of R ;
consider y being Element of R such that
A4: xx <= y by A3;
take y ; :: thesis: ( y in the carrier of R & [x,y] in the InternalRel of R )
thus ( y in the carrier of R & [x,y] in the InternalRel of R ) by A4, ORDERS_2:def 5; :: thesis: verum

end;

hence R is serial ; :: thesis: verum