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