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 ((),b)) /\ N by ;
c in Class ((),b) by ;
then [c,b] in EqRel R by EQREL_1:19;
then [c,b] in the InternalRel of R /\ ( the InternalRel of R ~) by ;
then A6: [c,b] in the InternalRel of R by XBOOLE_0:def 4;
A7: now :: thesis: for d being set holds
( not d in N or not d <> c or not [d,c] in the InternalRel of (R \~) )
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 ;
R is transitive by A1;
then A11: the InternalRel of R is_transitive_in the carrier of R ;
then A12: [d,b] in the InternalRel of R by A6, A8, A9;
now :: thesis: not [d,b] in the InternalRel of R ~
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;
hence contradiction by A10, RELAT_1:def 7; :: thesis: verum
end;
then A13: [d,b] in the InternalRel of (R \~) by ;
b <> d by ;
hence contradiction by A4, A8, A13, WAYBEL_4:def 25; :: thesis: verum
end;
c in N by ;
hence c is_minimal_wrt N, the InternalRel of (R \~) by ; :: thesis: verum