let R be RelStr ; :: thesis: ( R is well_founded implies R \~ is well_founded )
assume A1: R is well_founded ; :: thesis:
set IR = the InternalRel of R;
set CR = the carrier of R;
set IR9 = the InternalRel of (R \~);
set CR9 = the carrier of (R \~);
A2: the InternalRel of R is_well_founded_in the carrier of R by ;
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
A3: Y c= the carrier of (R \~) and
A4: Y <> {} ; :: thesis: ex a being object st
( a in Y & the InternalRel of (R \~) -Seg a misses Y )

consider a being object such that
A5: a in Y and
A6: the InternalRel of R -Seg a misses Y by ;
A7: ( the InternalRel of R -Seg a) /\ Y = {} by ;
take a = a; :: thesis: ( a in Y & the InternalRel of (R \~) -Seg a misses Y )
thus a in Y by A5; :: thesis: the InternalRel of (R \~) -Seg a misses Y
now :: thesis: for z being object holds not z in ( the InternalRel of (R \~) -Seg a) /\ Y
given z being object such that A8: z in ( the InternalRel of (R \~) -Seg a) /\ Y ; :: thesis: contradiction
A9: z in the InternalRel of (R \~) -Seg a by ;
A10: z in Y by ;
A11: z <> a by ;
[z,a] in the InternalRel of (R \~) by ;
then z in the InternalRel of R -Seg a by ;
hence contradiction by A7, A10, XBOOLE_0:def 4; :: thesis: verum
end;
then ( the InternalRel of (R \~) -Seg a) /\ Y = {} by XBOOLE_0:def 1;
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