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;

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

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 \~) )

c in N
by A3, A5, XBOOLE_0:def 4;( 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;

b <> d by A6, A10, RELAT_1:def 7;

hence contradiction by A4, A8, A13, WAYBEL_4:def 25; :: thesis: verum

end;( 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 ~

then A13:
[d,b] in the InternalRel of (R \~)
by A12, XBOOLE_0:def 5;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 [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

b <> d by A6, A10, RELAT_1:def 7;

hence contradiction by A4, A8, A13, WAYBEL_4:def 25; :: thesis: verum

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