let R be non empty RelStr ; :: thesis: ( R \~ is well_founded iff for N being Subset of R st N <> {} holds
ex x being object st x in min-classes N )
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);
set CR9 = the carrier of (R \~);

hereby :: thesis: ( ( for N being Subset of R st N <> {} holds
ex x being object st x in min-classes N ) implies R \~ is well_founded )

assume R \~ is well_founded ; :: thesis: for N being Subset of the carrier of R st N <> {} holds
ex x being object st x in min-classes N
then A1: the InternalRel of (R \~) is_well_founded_in the carrier of (R \~) by WELLFND1:def 2;
let N be Subset of the carrier of R; :: thesis: ( N <> {} implies ex x being object st x in min-classes N )
assume A2: N <> {} ; :: thesis: ex x being object st x in min-classes N
reconsider N9 = N as Subset of the carrier of (R \~) ;
consider y being object such that
A3: y in N9 and
A4: the InternalRel of (R \~) -Seg y misses N9 by A1, A2, WELLORD1:def 3;
A5: ( the InternalRel of (R \~) -Seg y) /\ N9 = {} by A4, XBOOLE_0:def 7;
reconsider y = y as Element of (R \~) by A3;
set x = (Class ((EqRel R),y)) /\ N;

now :: thesis: for z being set holds
( not z in N or not z <> y or not [z,y] in the InternalRel of (R \~) )

assume ex z being set st
( z in N & z <> y & [z,y] in the InternalRel of (R \~) ) ; :: thesis: contradiction
then consider z being set such that
A6: z in N and
A7: z <> y and
A8: [z,y] in the InternalRel of (R \~) ;
z in the InternalRel of (R \~) -Seg y by A7, A8, WELLORD1:1;
hence contradiction by A5, A6, XBOOLE_0:def 4; :: thesis: verum

end;

then y is_minimal_wrt N, the InternalRel of (R \~) by A3, WAYBEL_4:def 25;
then (Class ((EqRel R),y)) /\ N in min-classes N by Def8;
hence ex x being object st x in min-classes N ; :: thesis: verum

end;

assume A9: for N being Subset of R st N <> {} holds
ex x being object st x in min-classes N ; :: thesis: R \~ is well_founded

now :: thesis: for N being set st N c= the carrier of (R \~) & N <> {} holds
ex a9 being object st
( a9 in N & the InternalRel of (R \~) -Seg a9 misses N )

let N be set ; :: thesis: ( N c= the carrier of (R \~) & N <> {} implies ex a9 being object st
( a9 in N & the InternalRel of (R \~) -Seg a9 misses N ) )
assume that
A10: N c= the carrier of (R \~) and
A11: N <> {} ; :: thesis: ex a9 being object st
( a9 in N & the InternalRel of (R \~) -Seg a9 misses N )
reconsider N9 = N as Subset of R by A10;
consider x being object such that
A12: x in min-classes N9 by A9, A11;
consider a being Element of (R \~) such that
A13: a is_minimal_wrt N9, the InternalRel of (R \~) and
x = (Class ((EqRel R),a)) /\ N9 by A12, Def8;
reconsider a9 = a as object ;
take a9 = a9; :: thesis: ( a9 in N & the InternalRel of (R \~) -Seg a9 misses N )
thus a9 in N by A13, WAYBEL_4:def 25; :: thesis: the InternalRel of (R \~) -Seg a9 misses N

now :: thesis: not ( the InternalRel of (R \~) -Seg a9) /\ N <> {}

assume ( the InternalRel of (R \~) -Seg a9) /\ N <> {} ; :: thesis: contradiction
then consider z being object such that
A14: z in ( the InternalRel of (R \~) -Seg a9) /\ N by XBOOLE_0:def 1;
A15: z in the InternalRel of (R \~) -Seg a9 by A14, XBOOLE_0:def 4;
A16: z in N by A14, XBOOLE_0:def 4;
then reconsider z = z as Element of (R \~) by A10;
A17: z <> a9 by A15, WELLORD1:1;
[z,a] in the InternalRel of (R \~) by A15, WELLORD1:1;
hence contradiction by A13, A16, A17, WAYBEL_4:def 25; :: thesis: verum

end;

hence the InternalRel of (R \~) -Seg a9 misses N by XBOOLE_0:def 7; :: thesis: verum

end;

then the InternalRel of (R \~) is_well_founded_in the carrier of (R \~) by WELLORD1:def 3;
hence R \~ is well_founded by WELLFND1:def 2; :: thesis: verum