let R be RelStr ; :: thesis: for N being Subset of R
for x being Element of (R \~) st R is quasi_ordered & x in N & ( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x) holds
x is_minimal_wrt N, the InternalRel of (R \~)
let N be Subset of R; :: thesis: for x being Element of (R \~) st R is quasi_ordered & x in N & ( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x) holds
x is_minimal_wrt N, the InternalRel of (R \~)
let x be Element of (R \~); :: thesis: ( R is quasi_ordered & x in N & ( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x) implies x is_minimal_wrt N, the InternalRel of (R \~) )
assume that
A1: R is quasi_ordered and
A2: x in N and
A3: ( the InternalRel of R -Seg x) /\ N c= Class ((EqRel R),x) ; :: thesis: x is_minimal_wrt N, the InternalRel of (R \~)
set IR = the InternalRel of R;
set IR9 = the InternalRel of (R \~);

now :: thesis: for y being set holds
( not y in N or not y <> x or not [y,x] in the InternalRel of (R \~) )

assume ex y being set st
( y in N & y <> x & [y,x] in the InternalRel of (R \~) ) ; :: thesis: contradiction
then consider y being set such that
A4: y in N and
A5: y <> x and
A6: [y,x] in the InternalRel of (R \~) ;
A7: not [y,x] in the InternalRel of R ~ by A6, XBOOLE_0:def 5;
y in the InternalRel of R -Seg x by A5, A6, WELLORD1:1;
then y in ( the InternalRel of R -Seg x) /\ N by A4, XBOOLE_0:def 4;
then [y,x] in EqRel R by A3, EQREL_1:19;
then [y,x] in the InternalRel of R /\ ( the InternalRel of R ~) by A1, Def4;
hence contradiction by A7, XBOOLE_0:def 4; :: thesis: verum

end;

hence x is_minimal_wrt N, the InternalRel of (R \~) by A2, WAYBEL_4:def 25; :: thesis: verum