let R be non empty RelStr ; :: thesis: for x being Element of R holds {x} is well_founded Subset of R
let x be Element of R; :: thesis: {x} is well_founded Subset of R
set r = the InternalRel of R;
reconsider sx = {x} as Subset of R ;
sx is well_founded

proof

let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis: ( not Y c= sx or Y = {} or ex b₁ being object st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y ) )
assume that
A1: Y c= sx and
A2: Y <> {} ; :: thesis: ex b₁ being object st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y )
take x ; :: thesis: ( x in Y & the InternalRel of R -Seg x misses Y )
Y = sx by A1, A2, ZFMISC_1:33;
hence x in Y by TARSKI:def 1; :: thesis: the InternalRel of R -Seg x misses Y
assume not the InternalRel of R -Seg x misses Y ; :: thesis: contradiction
then consider a being object such that
A3: a in ( the InternalRel of R -Seg x) /\ Y by XBOOLE_0:4;
a in the InternalRel of R -Seg x by A3, XBOOLE_0:def 4;
then A4: a <> x by WELLORD1:1;
a in Y by A3, XBOOLE_0:def 4;
hence contradiction by A1, A4, TARSKI:def 1; :: thesis: verum

end;

hence {x} is well_founded Subset of R ; :: thesis: verum