let R be RelStr ; :: thesis: ( R is well_founded implies R \~ is well_founded )

assume A1: R is well_founded ; :: thesis: R \~ is well_founded

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 A1, WELLFND1:def 2;

hence R \~ is well_founded by WELLFND1:def 2; :: thesis: verum

assume A1: R is well_founded ; :: thesis: R \~ is well_founded

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 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 )

then
the InternalRel of (R \~) is_well_founded_in the carrier of (R \~)
by WELLORD1:def 3;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 A2, A3, A4, WELLORD1:def 3;

A7: ( the InternalRel of R -Seg a) /\ Y = {} by A6, XBOOLE_0:def 7;

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

hence the InternalRel of (R \~) -Seg a misses Y by XBOOLE_0:def 7; :: thesis: verum

end;( 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 A2, A3, A4, WELLORD1:def 3;

A7: ( the InternalRel of R -Seg a) /\ Y = {} by A6, XBOOLE_0:def 7;

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

then
( the InternalRel of (R \~) -Seg a) /\ Y = {}
by XBOOLE_0:def 1;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 A8, XBOOLE_0:def 4;

A10: z in Y by A8, XBOOLE_0:def 4;

A11: z <> a by A9, WELLORD1:1;

[z,a] in the InternalRel of (R \~) by A9, WELLORD1:1;

then z in the InternalRel of R -Seg a by A11, WELLORD1:1;

hence contradiction by A7, A10, XBOOLE_0:def 4; :: thesis: verum

end;A9: z in the InternalRel of (R \~) -Seg a by A8, XBOOLE_0:def 4;

A10: z in Y by A8, XBOOLE_0:def 4;

A11: z <> a by A9, WELLORD1:1;

[z,a] in the InternalRel of (R \~) by A9, WELLORD1:1;

then z in the InternalRel of R -Seg a by A11, WELLORD1:1;

hence contradiction by A7, A10, XBOOLE_0:def 4; :: thesis: verum

hence the InternalRel of (R \~) -Seg a misses Y by XBOOLE_0:def 7; :: thesis: verum

hence R \~ is well_founded by WELLFND1:def 2; :: thesis: verum