let X be set ; :: thesis: for R being Relation st R is well_founded holds

R |_2 X is well_founded

let R be Relation; :: thesis: ( R is well_founded implies R |_2 X is well_founded )

assume A1: for Y being set st Y c= field R & Y <> {} holds

ex a being object st

( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def 2 :: thesis: R |_2 X is well_founded

A2: field (R |_2 X) c= field R by Th13;

let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( Y c= field (R |_2 X) & Y <> {} implies ex a being object st

( a in Y & (R |_2 X) -Seg a misses Y ) )

assume ( Y c= field (R |_2 X) & Y <> {} ) ; :: thesis: ex a being object st

( a in Y & (R |_2 X) -Seg a misses Y )

then consider a being object such that

A3: a in Y and

A4: R -Seg a misses Y by A1, A2, XBOOLE_1:1;

take a ; :: thesis: ( a in Y & (R |_2 X) -Seg a misses Y )

thus a in Y by A3; :: thesis: (R |_2 X) -Seg a misses Y

assume not (R |_2 X) -Seg a misses Y ; :: thesis: contradiction

then A5: ex b being object st

( b in (R |_2 X) -Seg a & b in Y ) by XBOOLE_0:3;

(R |_2 X) -Seg a c= R -Seg a by Th14;

hence contradiction by A4, A5, XBOOLE_0:3; :: thesis: verum

R |_2 X is well_founded

let R be Relation; :: thesis: ( R is well_founded implies R |_2 X is well_founded )

assume A1: for Y being set st Y c= field R & Y <> {} holds

ex a being object st

( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def 2 :: thesis: R |_2 X is well_founded

A2: field (R |_2 X) c= field R by Th13;

let Y be set ; :: according to WELLORD1:def 2 :: thesis: ( Y c= field (R |_2 X) & Y <> {} implies ex a being object st

( a in Y & (R |_2 X) -Seg a misses Y ) )

assume ( Y c= field (R |_2 X) & Y <> {} ) ; :: thesis: ex a being object st

( a in Y & (R |_2 X) -Seg a misses Y )

then consider a being object such that

A3: a in Y and

A4: R -Seg a misses Y by A1, A2, XBOOLE_1:1;

take a ; :: thesis: ( a in Y & (R |_2 X) -Seg a misses Y )

thus a in Y by A3; :: thesis: (R |_2 X) -Seg a misses Y

assume not (R |_2 X) -Seg a misses Y ; :: thesis: contradiction

then A5: ex b being object st

( b in (R |_2 X) -Seg a & b in Y ) by XBOOLE_0:3;

(R |_2 X) -Seg a c= R -Seg a by Th14;

hence contradiction by A4, A5, XBOOLE_0:3; :: thesis: verum