let R be non empty RelStr ; :: thesis:
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);
set CR9 = the carrier of (R \~);

hereby :: thesis:

assume R \~ is well_founded ; :: thesis:
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:
assume A2: N <> {} ; :: thesis:
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:

assume ex z being set st
( z in N & z <> y & [z,y] in the InternalRel of (R \~) ) ; :: thesis:
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:

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:

end;

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

now :: thesis:

let N be set ; :: thesis:
assume that
A10: N c= the carrier of (R \~) and
A11: N <> {} ; :: thesis:
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:
thus a9 in N by A13, WAYBEL_4:def 25; :: thesis:

now :: thesis:

assume ( the InternalRel of (R \~) -Seg a9) /\ N <> {} ; :: thesis:
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:

end;

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

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: