let Y be TopStruct ; :: thesis: for A, B being Subset of Y st ( A is discrete or B is discrete ) holds
A /\ B is discrete
let A, B be Subset of Y; :: thesis: ( ( A is discrete or B is discrete ) implies A /\ B is discrete )
assume A1: ( A is discrete or B is discrete ) ; :: thesis: A /\ B is discrete
hereby :: thesis: verum
per cases ( A is discrete or B is discrete ) by A1;
end;
end;