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 b1 being object st
( b1 in Y & the InternalRel of R -Seg b1 misses Y ) )

assume that
A1: Y c= sx and
A2: Y <> {} ; :: thesis: ex b1 being object st
( b1 in Y & the InternalRel of R -Seg b1 misses Y )

take x ; :: thesis: ( x in Y & the InternalRel of R -Seg x misses Y )
Y = sx by ;
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 ;
then A4: a <> x by WELLORD1:1;
a in Y by ;
hence contradiction by A1, A4, TARSKI:def 1; :: thesis: verum
end;
hence {x} is well_founded Subset of R ; :: thesis: verum