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 5;

now

A3: ( a in (the InternalRel of L -Seg x) /\ N & ( for y being set holds
( not y in (the InternalRel of L -Seg x) /\ N or not a <> y or not [y,a] in the InternalRel of L ) ) ) by A1, WAYBEL_4:def 26;
then ( a in the InternalRel of L -Seg x & a in N ) by XBOOLE_0:def 4;
then A4: ( a <> x & [a,x] in the InternalRel of L ) by WELLORD1:def 1;
then reconsider a' = a as Element of L by ZFMISC_1:106;
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

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
A5: ( y in N & y <> a & [y,a] in the InternalRel of L ) ;
( a in the carrier of L & y in the carrier of L ) by A5, ZFMISC_1:106;
then A6: [y,x] in the InternalRel of L by A2, A4, A5, RELAT_2:def 8;

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

suppose x = y ; :: thesis: contradiction

then ( x <= a' & a' <= x ) by A4, A5, ORDERS_2:def 9;
hence contradiction by A4, ORDERS_2:25; :: thesis: verum

end;

suppose x <> y ; :: thesis: contradiction

then y in the InternalRel of L -Seg x by A6, WELLORD1:def 1;
then y in (the InternalRel of L -Seg x) /\ N by A5, XBOOLE_0:def 4;
hence contradiction by A1, A5, WAYBEL_4:def 26; :: 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 26; :: thesis: verum