let R be non empty RelStr ; :: thesis: ( R \~ is well_founded iff for N being Subset of R st N <> {} holds
ex x being set 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 set 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 set 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 set st x in min-classes N )
assume A2: N <> {} ; :: thesis: ex x being set st x in min-classes N
reconsider N9 = N as Subset of the carrier of (R \~ ) ;
consider y being set 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

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:def 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 26;
then (Class (EqRel R),y) /\ N in min-classes N by Def8;
hence ex x being set st x in min-classes N ; :: thesis: verum

end;

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

now

let N be set ; :: thesis: ( N c= the carrier of (R \~ ) & N <> {} implies ex a9 being set 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 set st
( a9 in N & the InternalRel of (R \~ ) -Seg a9 misses N )
reconsider N9 = N as Subset of R by A10;
consider x being set 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 set ;
take a9 = a9; :: thesis: ( a9 in N & the InternalRel of (R \~ ) -Seg a9 misses N )
thus a9 in N by A13, WAYBEL_4:def 26; :: thesis: the InternalRel of (R \~ ) -Seg a9 misses N

now

assume (the InternalRel of (R \~ ) -Seg a9) /\ N <> {} ; :: thesis: contradiction
then consider z being set 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:def 1;
[z,a] in the InternalRel of (R \~ ) by A15, WELLORD1:def 1;
hence contradiction by A13, A16, A17, WAYBEL_4:def 26; :: 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