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

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

hence
{x} is well_founded Subset of R
; :: thesis: verum
let Y be set ; :: according to WELLORD1:def 3,WELLFND1:def 3 :: thesis: ( not Y c= sx or Y = {} or ex b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} misses Y ) )

assume that

A1: Y c= sx and

A2: Y <> {} ; :: thesis: ex b_{1} being object st

( b_{1} in Y & the InternalRel of R -Seg b_{1} 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;( b

assume that

A1: Y c= sx and

A2: Y <> {} ; :: thesis: ex b

( b

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