reconsider er = {} as Relation of {{} } by RELSET_1:25;
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 set st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y ) )
assume ( Y c= the carrier of R & Y <> {} ) ; :: thesis: ex b₁ being set st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y )
then A1: Y = {{} } by ZFMISC_1:39;
take e = {} ; :: thesis: ( e in Y & the InternalRel of R -Seg e misses Y )
thus e in Y by A1, 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 set 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 & x in Y ) by A2, XBOOLE_0:def 4;
hence contradiction by WELLORD1:def 1; :: thesis: verum