reconsider e = {} as Subset of R by XBOOLE_1:2;

take e ; :: thesis: e is well_founded

let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis: ( not Y c= e or Y = {} or ex b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y ) )

assume ( Y c= e & Y <> {} ) ; :: thesis: ex b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y )

hence ex b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y )
; :: thesis: verum

take e ; :: thesis: e is well_founded

let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis: ( not Y c= e or Y = {} or ex b

( b

assume ( Y c= e & Y <> {} ) ; :: thesis: ex b

( b

hence ex b

( b