let L be RelStr ; :: thesis: ( ( for x, y being Element of L holds
( x <= y iff x c= y ) ) implies the InternalRel of L = RelIncl the carrier of L )
assume A1: for x, y being Element of L holds
( x <= y iff x c= y ) ; :: thesis: the InternalRel of L = RelIncl the carrier of L
for x being set st x in the carrier of L holds
ex y being set st [x,y] in the InternalRel of L

proof

let x be set ; :: thesis: ( x in the carrier of L implies ex y being set st [x,y] in the InternalRel of L )
assume x in the carrier of L ; :: thesis: ex y being set st [x,y] in the InternalRel of L
then reconsider x' = x as Element of L ;
take y = x'; :: thesis: [x,y] in the InternalRel of L
x' <= y by A1;
hence [x,y] in the InternalRel of L by ORDERS_2:def 9; :: thesis: verum

end;

then A2: dom the InternalRel of L = the carrier of L by RELSET_1:22;
for y being set st y in the carrier of L holds
ex x being set st [x,y] in the InternalRel of L

proof

let y be set ; :: thesis: ( y in the carrier of L implies ex x being set st [x,y] in the InternalRel of L )
assume y in the carrier of L ; :: thesis: ex x being set st [x,y] in the InternalRel of L
then reconsider y' = y as Element of L ;
take x = y'; :: thesis: [x,y] in the InternalRel of L
x <= y' by A1;
hence [x,y] in the InternalRel of L by ORDERS_2:def 9; :: thesis: verum

end;

then A3: field the InternalRel of L = the carrier of L \/ the carrier of L by A2, RELSET_1:23;

now

let Y, Z be set ; :: thesis: ( Y in the carrier of L & Z in the carrier of L implies ( ( [Y,Z] in the InternalRel of L implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of L ) ) )
assume ( Y in the carrier of L & Z in the carrier of L ) ; :: thesis: ( ( [Y,Z] in the InternalRel of L implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of L ) )
then reconsider Y' = Y, Z' = Z as Element of L ;
thus ( [Y,Z] in the InternalRel of L implies Y c= Z ) :: thesis: ( Y c= Z implies [Y,Z] in the InternalRel of L )

proof

assume [Y,Z] in the InternalRel of L ; :: thesis: Y c= Z
then Y' <= Z' by ORDERS_2:def 9;
hence Y c= Z by A1; :: thesis: verum

end;

thus ( Y c= Z implies [Y,Z] in the InternalRel of L ) :: thesis: verum

proof

assume Y c= Z ; :: thesis: [Y,Z] in the InternalRel of L
then Y' <= Z' by A1;
hence [Y,Z] in the InternalRel of L by ORDERS_2:def 9; :: thesis: verum

end;

end;

hence the InternalRel of L = RelIncl the carrier of L by A3, WELLORD2:def 1; :: thesis: verum