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 A1: ( Y = X \/ {x} & the InternalRel of R -Seg x c= X ) ; :: thesis: Y is lower
let z, y be set ; :: according to WELLFND1:def 1 :: thesis: ( z in Y & [y,z] in the InternalRel of R implies y in Y )
assume A2: ( z in Y & [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, A2, XBOOLE_0:def 3;

suppose z in X ; :: thesis: y in Y

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

end;

suppose ( z in {x} & y = z ) ; :: thesis: y in Y

hence y in Y by A2; :: thesis: verum

end;

suppose A3: ( 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 A2, A3, WELLORD1:def 1;
hence y in Y by A1, XBOOLE_0:def 3; :: thesis: verum

end;

end;