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 set st
( b₁ in Y & the InternalRel of R -Seg b₁ misses Y ) )
assume A1: ( Y c= sx & Y <> {} ) ; :: thesis: ex b₁ being set 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, ZFMISC_1:39;
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 set such that
A2: a in (the InternalRel of R -Seg x) /\ Y by XBOOLE_0:4;
( a in the InternalRel of R -Seg x & a in Y ) by A2, XBOOLE_0:def 4;
then ( a <> x & a = x ) by A1, TARSKI:def 1, WELLORD1:def 1;
hence contradiction ; :: thesis: verum

end;

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