let L be non empty transitive antisymmetric RelStr ; :: thesis:
let x be Element of L; :: thesis:
let a, N be set ; :: thesis:
assume A1: a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L ; :: thesis:
set IR = the InternalRel of L;
set CR = the carrier of L;
A2: the InternalRel of L is_transitive_in the carrier of L by ORDERS_2:def 3;

A3: a in ( the InternalRel of L -Seg x) /\ N by A1, WAYBEL_4:def 25;
then A4: a in the InternalRel of L -Seg x by XBOOLE_0:def 4;
then A5: a <> x by WELLORD1:1;
A6: [a,x] in the InternalRel of L by A4, WELLORD1:1;
then reconsider a9 = a as Element of L by ZFMISC_1:87;
thus a in N by A3, XBOOLE_0:def 4; :: thesis:

assume ex y being set st
( y in N & y <> a & [y,a] in the InternalRel of L ) ; :: thesis:
then consider y being set such that
A7: y in N and
A8: y <> a and
A9: [y,a] in the InternalRel of L ;
A10: a in the carrier of L by A9, ZFMISC_1:87;
y in the carrier of L by A9, ZFMISC_1:87;
then A11: [y,x] in the InternalRel of L by A2, A6, A9, A10;

suppose x = y ; :: thesis:

then A12: x <= a9 by A9;
a9 <= x by A6;
hence contradiction by A5, A12, ORDERS_2:2; :: thesis:

end;

suppose x <> y ; :: thesis:

then y in the InternalRel of L -Seg x by A11, WELLORD1:1;
then y in ( the InternalRel of L -Seg x) /\ N by A7, XBOOLE_0:def 4;
hence contradiction by A1, A8, A9, WAYBEL_4:def 25; :: thesis:

end;

end;

end;

hence for y being set holds
( not y in N or not y <> a or not [y,a] in the InternalRel of L ) ; :: thesis:

end;

hence a is_minimal_wrt N, the InternalRel of L by WAYBEL_4:def 25; :: thesis: