reconsider er = {} as Relation of {{}} by RELSET_1:12;

take R = RelStr(# {{}},er #); :: thesis: ( not R is empty & R is well_founded )

thus not R is empty ; :: thesis: R is well_founded

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

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

assume A1: ( Y c= the carrier of R & Y <> {} ) ; :: thesis: ex b_{1} being object st

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

take e = {} ; :: thesis: ( e in Y & the InternalRel of R -Seg e misses Y )

Y = {{}} by A1, ZFMISC_1:33;

hence e in Y by TARSKI:def 1; :: thesis: the InternalRel of R -Seg e misses Y

assume ( the InternalRel of R -Seg e) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A2: x in ( the InternalRel of R -Seg e) /\ Y by XBOOLE_0:def 1;

x in the InternalRel of R -Seg e by A2, XBOOLE_0:def 4;

hence contradiction by WELLORD1:1; :: thesis: verum

take R = RelStr(# {{}},er #); :: thesis: ( not R is empty & R is well_founded )

thus not R is empty ; :: thesis: R is well_founded

let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 2 :: thesis: ( not Y c= the carrier of R or Y = {} or ex b

( b

assume A1: ( Y c= the carrier of R & Y <> {} ) ; :: thesis: ex b

( b

take e = {} ; :: thesis: ( e in Y & the InternalRel of R -Seg e misses Y )

Y = {{}} by A1, ZFMISC_1:33;

hence e in Y by TARSKI:def 1; :: thesis: the InternalRel of R -Seg e misses Y

assume ( the InternalRel of R -Seg e) /\ Y <> {} ; :: according to XBOOLE_0:def 7 :: thesis: contradiction

then consider x being object such that

A2: x in ( the InternalRel of R -Seg e) /\ Y by XBOOLE_0:def 1;

x in the InternalRel of R -Seg e by A2, XBOOLE_0:def 4;

hence contradiction by WELLORD1:1; :: thesis: verum