let R be non empty RelStr ; :: thesis: for N being Subset of R
for x being set st R is quasi_ordered & x in min-classes N holds
for y being Element of (R \~ ) st y in x holds
y is_minimal_wrt N,the InternalRel of (R \~ )
let N be Subset of R; :: thesis: for x being set st R is quasi_ordered & x in min-classes N holds
for y being Element of (R \~ ) st y in x holds
y is_minimal_wrt N,the InternalRel of (R \~ )
let x be set ; :: thesis: ( R is quasi_ordered & x in min-classes N implies for y being Element of (R \~ ) st y in x holds
y is_minimal_wrt N,the InternalRel of (R \~ ) )
assume that
A1: R is quasi_ordered and
A2: x in min-classes N ; :: thesis: for y being Element of (R \~ ) st y in x holds
y is_minimal_wrt N,the InternalRel of (R \~ )
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~ );
let c be Element of (R \~ ); :: thesis: ( c in x implies c is_minimal_wrt N,the InternalRel of (R \~ ) )
assume A3: c in x ; :: thesis: c is_minimal_wrt N,the InternalRel of (R \~ )
consider b being Element of (R \~ ) such that
A4: b is_minimal_wrt N,the InternalRel of (R \~ ) and
A5: x = (Class (EqRel R),b) /\ N by A2, Def8;
c in Class (EqRel R),b by A3, A5, XBOOLE_0:def 4;
then [c,b] in EqRel R by EQREL_1:27;
then [c,b] in the InternalRel of R /\ (the InternalRel of R ~ ) by A1, Def4;
then A6: [c,b] in the InternalRel of R by XBOOLE_0:def 4;

A7: now

assume ex d being set st
( d in N & d <> c & [d,c] in the InternalRel of (R \~ ) ) ; :: thesis: contradiction
then consider d being set such that
A8: d in N and
d <> c and
A9: [d,c] in the InternalRel of (R \~ ) ;
A10: not [d,c] in the InternalRel of R ~ by A9, XBOOLE_0:def 5;
R is transitive by A1, Def3;
then A11: the InternalRel of R is_transitive_in the carrier of R by ORDERS_2:def 5;
then A12: [d,b] in the InternalRel of R by A6, A8, A9, RELAT_2:def 8;

now

assume [d,b] in the InternalRel of R ~ ; :: thesis: contradiction
then [b,d] in the InternalRel of R by RELAT_1:def 7;
then [c,d] in the InternalRel of R by A6, A8, A11, RELAT_2:def 8;
hence contradiction by A10, RELAT_1:def 7; :: thesis: verum

end;

then A13: [d,b] in the InternalRel of (R \~ ) by A12, XBOOLE_0:def 5;
b <> d by A6, A10, RELAT_1:def 7;
hence contradiction by A4, A8, A13, WAYBEL_4:def 26; :: thesis: verum

end;

c in N by A3, A5, XBOOLE_0:def 4;
hence c is_minimal_wrt N,the InternalRel of (R \~ ) by A7, WAYBEL_4:def 26; :: thesis: verum