let L be non empty transitive antisymmetric RelStr ; :: thesis: for x being Element of L
for a, N being set st a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L holds
a is_minimal_wrt N, the InternalRel of L
let x be Element of L; :: thesis: for a, N being set st a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L holds
a is_minimal_wrt N, the InternalRel of L
let a, N be set ; :: thesis: ( a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L implies a is_minimal_wrt N, the InternalRel of L )
assume A1: a is_minimal_wrt ( the InternalRel of L -Seg x) /\ N, the InternalRel of L ; :: thesis: a is_minimal_wrt N, the InternalRel of L
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;

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

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: for y being set holds
( not y in N or not y <> a or not [y,a] in the InternalRel of L )

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

assume ex y being set st
( y in N & y <> a & [y,a] in the InternalRel of L ) ; :: thesis: contradiction
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;

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: contradiction

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

end;

suppose x <> y ; :: thesis: contradiction

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: verum

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: verum

end;

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