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

A2: now :: thesis: for Y, Z being set st Y in the carrier of L & Z in the carrier of L holds
( ( [Y,Z] in the InternalRel of L implies Y c= Z ) & ( Y c= Z implies [Y,Z] in the InternalRel of L ) )

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 Y9 = Y, Z9 = 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 Y9 <= Z9 by ORDERS_2:def 5;
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 Y9 <= Z9 by A1;
hence [Y,Z] in the InternalRel of L by ORDERS_2:def 5; :: thesis: verum

end;

end;

for x being object st x in the carrier of L holds
ex y being object st [x,y] in the InternalRel of L

proof

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

end;

then A3: dom the InternalRel of L = the carrier of L by RELSET_1:9;
for y being object st y in the carrier of L holds
ex x being object st [x,y] in the InternalRel of L

proof

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

end;

then field the InternalRel of L = the carrier of L \/ the carrier of L by A3, RELSET_1:10;
hence the InternalRel of L = RelIncl the carrier of L by A2, WELLORD2:def 1; :: thesis: verum