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:19;
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 :: 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 A9, XBOOLE_0:def 5;
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 A12, XBOOLE_0:def 5;
b <> d by A6, A10, RELAT_1:def 7;
hence contradiction by A4, A8, A13, WAYBEL_4:def 25; :: 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 25; :: thesis: verum