let X be set ; :: thesis: for A being Subset of X
for A1 being SetSequence of X st A1 is monotone holds
A (/\) A1 is monotone
let A be Subset of X; :: thesis: for A1 being SetSequence of X st A1 is monotone holds
A (/\) A1 is monotone
let A1 be SetSequence of X; :: thesis: ( A1 is monotone implies A (/\) A1 is monotone )
assume A1: A1 is monotone ; :: thesis: A (/\) A1 is monotone
per cases ( A1 is non-ascending or A1 is non-descending ) by A1, SETLIM_1:def 1;
suppose A1 is non-ascending ; :: thesis: A (/\) A1 is monotone
then A (/\) A1 is non-ascending by Th21;
hence A (/\) A1 is monotone by SETLIM_1:def 1; :: thesis: verum
end;
suppose A1 is non-descending ; :: thesis: A (/\) A1 is monotone
then A (/\) A1 is non-descending by Th22;
hence A (/\) A1 is monotone by SETLIM_1:def 1; :: thesis: verum
end;
end;