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 ;
suppose z in X ; :: thesis: y in Y
then y in X by ;
hence y in Y by ; :: 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 ;
hence y in Y by ; :: thesis: verum
end;
end;