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 IR' = the InternalRel of (R \~ );
set CR' = 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 N' = N as Subset of the carrier of (R \~ ) ;
consider y being set such that
A3: y in N' and
A4: the InternalRel of (R \~ ) -Seg y misses N' by A1, A2, WELLORD1:def 3;
A5: (the InternalRel of (R \~ ) -Seg y) /\ N' = {} by A4, XBOOLE_0:def 7;
reconsider y = y as Element of (R \~ ) by A3;
set x = (Class (EqRel R),y) /\ N;

now

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

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 & z <> y ) and
A7: [z,y] in the InternalRel of (R \~ ) ;
z in the InternalRel of (R \~ ) -Seg y by A6, A7, WELLORD1:def 1;
hence contradiction by A5, A6, XBOOLE_0:def 4; :: thesis: verum

end;

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

end;

then y is_minimal_wrt N,the InternalRel of (R \~ ) by 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 A8: 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 a' being set st
( a' in N & the InternalRel of (R \~ ) -Seg a' misses N ) )
assume that
A9: N c= the carrier of (R \~ ) and
A10: N <> {} ; :: thesis: ex a' being set st
( a' in N & the InternalRel of (R \~ ) -Seg a' misses N )
reconsider N' = N as Subset of R by A9;
consider x being set such that
A11: x in min-classes N' by A8, A10;
consider a being Element of (R \~ ) such that
A12: a is_minimal_wrt N',the InternalRel of (R \~ ) and
x = (Class (EqRel R),a) /\ N' by A11, Def8;
reconsider a' = a as set ;
take a' = a'; :: thesis: ( a' in N & the InternalRel of (R \~ ) -Seg a' misses N )
thus a' in N by A12, WAYBEL_4:def 26; :: thesis: the InternalRel of (R \~ ) -Seg a' misses N

now

assume (the InternalRel of (R \~ ) -Seg a') /\ N <> {} ; :: thesis: contradiction
then consider z being set such that
A13: z in (the InternalRel of (R \~ ) -Seg a') /\ N by XBOOLE_0:def 1;
A14: ( z in the InternalRel of (R \~ ) -Seg a' & z in N ) by A13, XBOOLE_0:def 4;
then reconsider z = z as Element of (R \~ ) by A9;
( z <> a' & [z,a] in the InternalRel of (R \~ ) ) by A14, WELLORD1:def 1;
hence contradiction by A12, A14, WAYBEL_4:def 26; :: thesis: verum

end;

hence the InternalRel of (R \~ ) -Seg a' 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