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

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

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

then y in X by A4, 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 A3; :: thesis: verum

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;

end;