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 IR' = the InternalRel of (R \~ );

now

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: ( [y,x] in the InternalRel of R & 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:def 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:27;
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 26; :: thesis: verum