let R be Relation; :: thesis: ( R is well_founded iff R is_well_founded_in field R )
thus ( R is well_founded implies R is_well_founded_in field R ) :: thesis: ( R is_well_founded_in field R implies R is well_founded )

proof

assume for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def 2 :: thesis: R is_well_founded_in field R
hence for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def 3 :: thesis: verum

end;

assume for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def 3 :: thesis: R is well_founded
hence for Y being set st Y c= field R & Y <> {} holds
ex a being set st
( a in Y & R -Seg a misses Y ) ; :: according to WELLORD1:def 2 :: thesis: verum