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₁ being object st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y ) )
assume ( Y c= e & Y <> {} ) ; :: thesis: ex b₁ being object st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y )
hence ex b₁ being object st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y ) ; :: thesis: verum