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