let R be RelStr ; :: thesis: ( R \~ is well_founded & R is antisymmetric implies R is well_founded )
assume that
A1: R \~ is well_founded and
A2: R is antisymmetric ; :: thesis: R is well_founded
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);
A3: the InternalRel of R is_antisymmetric_in the carrier of R by A2;
A4: the InternalRel of (R \~) is_well_founded_in the carrier of R by A1, WELLFND1:def 2;

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

let Y be set ; :: thesis: ( Y c= the carrier of R & Y <> {} implies ex a being object st
( a in Y & the InternalRel of R -Seg a misses Y ) )
assume that
A5: Y c= the carrier of R and
A6: Y <> {} ; :: thesis: ex a being object st
( a in Y & the InternalRel of R -Seg a misses Y )
consider a being object such that
A7: a in Y and
A8: the InternalRel of (R \~) -Seg a misses Y by A4, A5, A6, WELLORD1:def 3;
A9: ( the InternalRel of (R \~) -Seg a) /\ Y = {} by A8, XBOOLE_0:def 7;
take a = a; :: thesis: ( a in Y & the InternalRel of R -Seg a misses Y )
thus a in Y by A7; :: thesis: the InternalRel of R -Seg a misses Y

now :: thesis: not ( the InternalRel of R -Seg a) /\ Y <> {}

assume ( the InternalRel of R -Seg a) /\ Y <> {} ; :: thesis: contradiction
then consider z being object such that
A10: z in ( the InternalRel of R -Seg a) /\ Y by XBOOLE_0:def 1;
A11: z in the InternalRel of R -Seg a by A10, XBOOLE_0:def 4;
A12: z in Y by A10, XBOOLE_0:def 4;
A13: z <> a by A11, WELLORD1:1;
A14: [z,a] in the InternalRel of R by A11, WELLORD1:1;
then not [a,z] in the InternalRel of R by A3, A5, A7, A12, A13;
then not [z,a] in the InternalRel of R ~ by RELAT_1:def 7;
then [z,a] in the InternalRel of R \ ( the InternalRel of R ~) by A14, XBOOLE_0:def 5;
then z in the InternalRel of (R \~) -Seg a by A13, WELLORD1:1;
hence contradiction by A9, A12, XBOOLE_0:def 4; :: thesis: verum

end;

hence the InternalRel of R -Seg a misses Y 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