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;

suppose A is discrete ; :: thesis: A /\ B is discrete

hence A /\ B is discrete by Th22, XBOOLE_1:17; :: thesis: verum

end;

suppose B is discrete ; :: thesis: A /\ B is discrete

hence A /\ B is discrete by Th22, XBOOLE_1:17; :: thesis: verum

end;

end;

end;