let Y be TopStruct ; :: thesis: ( ( for P, Q being Subset of Y st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) ) implies for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete )
assume A1: for P, Q being Subset of Y st P is open & Q is open holds
( P /\ Q is open & P \/ Q is open ) ; :: thesis: for A, B being Subset of Y st A is open & B is open & A is discrete & B is discrete holds
A \/ B is discrete
let A, B be Subset of Y; :: thesis: ( A is open & B is open & A is discrete & B is discrete implies A \/ B is discrete )
assume A2: ( A is open & B is open ) ; :: thesis: ( not A is discrete or not B is discrete or A \/ B is discrete )
assume A3: ( A is discrete & B is discrete ) ; :: thesis: A \/ B is discrete

now

let D be Subset of Y; :: thesis: ( D c= A \/ B implies ex G being Subset of Y st
( G is open & (A \/ B) /\ G = D ) )
assume D c= A \/ B ; :: thesis: ex G being Subset of Y st
( G is open & (A \/ B) /\ G = D )
then A4: D = D /\ (A \/ B) by XBOOLE_1:28;
D /\ A c= A by XBOOLE_1:17;
then consider G1 being Subset of Y such that
A5: G1 is open and
A6: A /\ G1 = D /\ A by A3, Def5;
D /\ B c= B by XBOOLE_1:17;
then consider G2 being Subset of Y such that
A7: G2 is open and
A8: B /\ G2 = D /\ B by A3, Def5;

now

take G = (A /\ G1) \/ (B /\ G2); :: thesis: ( G is open & (A \/ B) /\ G = D )
( A /\ G1 is open & B /\ G2 is open ) by A1, A2, A5, A7;
hence G is open by A1; :: thesis: (A \/ B) /\ G = D
thus (A \/ B) /\ G = D by A4, A6, A8, XBOOLE_1:23; :: thesis: verum

end;

hence ex G being Subset of Y st
( G is open & (A \/ B) /\ G = D ) ; :: thesis: verum

end;

hence A \/ B is discrete by Def5; :: thesis: verum