let R be RelStr ; :: thesis: for X being lower Subset of R

for Y being Subset of R

for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds

Y is lower

let X be lower Subset of R; :: thesis: for Y being Subset of R

for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds

Y is lower

let Y be Subset of R; :: thesis: for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds

Y is lower

let x be set ; :: thesis: ( Y = X \/ {x} & the InternalRel of R -Seg x c= X implies Y is lower )

set r = the InternalRel of R;

assume that

A1: Y = X \/ {x} and

A2: the InternalRel of R -Seg x c= X ; :: thesis: Y is lower

let z, y be object ; :: according to WELLFND1:def 1 :: thesis: ( z in Y & [y,z] in the InternalRel of R implies y in Y )

assume that

A3: z in Y and

A4: [y,z] in the InternalRel of R ; :: thesis: y in Y

for Y being Subset of R

for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds

Y is lower

let X be lower Subset of R; :: thesis: for Y being Subset of R

for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds

Y is lower

let Y be Subset of R; :: thesis: for x being set st Y = X \/ {x} & the InternalRel of R -Seg x c= X holds

Y is lower

let x be set ; :: thesis: ( Y = X \/ {x} & the InternalRel of R -Seg x c= X implies Y is lower )

set r = the InternalRel of R;

assume that

A1: Y = X \/ {x} and

A2: the InternalRel of R -Seg x c= X ; :: thesis: Y is lower

let z, y be object ; :: according to WELLFND1:def 1 :: thesis: ( z in Y & [y,z] in the InternalRel of R implies y in Y )

assume that

A3: z in Y and

A4: [y,z] in the InternalRel of R ; :: thesis: y in Y

per cases
( z in X or ( z in {x} & y = z ) or ( z in {x} & y <> z ) )
by A1, A3, XBOOLE_0:def 3;

end;

suppose A5:
( z in {x} & y <> z )
; :: thesis: y in Y

then
z = x
by TARSKI:def 1;

then y in the InternalRel of R -Seg x by A4, A5, WELLORD1:1;

hence y in Y by A1, A2, XBOOLE_0:def 3; :: thesis: verum

end;then y in the InternalRel of R -Seg x by A4, A5, WELLORD1:1;

hence y in Y by A1, A2, XBOOLE_0:def 3; :: thesis: verum