let Y be TopStruct ; :: thesis: ( ( for P, Q being Subset of Y st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ) implies for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete )
assume A1: for P, Q being Subset of Y st P is closed & Q is closed holds
( P /\ Q is closed & P \/ Q is closed ) ; :: thesis: for A, B being Subset of Y st A is closed & B is closed & A is discrete & B is discrete holds
A \/ B is discrete
let A, B be Subset of Y; :: thesis: ( A is closed & B is closed & A is discrete & B is discrete implies A \/ B is discrete )
assume that
A2: A is closed and
A3: B is closed ; :: thesis: ( not A is discrete or not B is discrete or A \/ B is discrete )
assume that
A4: A is discrete and
A5: B is discrete ; :: thesis: A \/ B is discrete
now :: thesis: for D being Subset of Y st D c= A \/ B holds
ex F being Subset of Y st
( F is closed & (A \/ B) /\ F = D )
let D be Subset of Y; :: thesis: ( D c= A \/ B implies ex F being Subset of Y st
( F is closed & (A \/ B) /\ F = D ) )
D /\ A c= A by XBOOLE_1:17;
then consider F1 being Subset of Y such that
A6: F1 is closed and
A7: A /\ F1 = D /\ A by A4;
D /\ B c= B by XBOOLE_1:17;
then consider F2 being Subset of Y such that
A8: F2 is closed and
A9: B /\ F2 = D /\ B by A5;
assume D c= A \/ B ; :: thesis: ex F being Subset of Y st
( F is closed & (A \/ B) /\ F = D )
then A10: D = D /\ (A \/ B) by XBOOLE_1:28;
now :: thesis: ex F being Element of bool the carrier of Y st
( F is closed & (A \/ B) /\ F = D )
take F = (A /\ F1) \/ (B /\ F2); :: thesis: ( F is closed & (A \/ B) /\ F = D )
A11: B /\ F2 is closed by A1, A3, A8;
A /\ F1 is closed by A1, A2, A6;
hence F is closed by A1, A11; :: thesis: (A \/ B) /\ F = D
thus (A \/ B) /\ F = D by A10, A7, A9, XBOOLE_1:23; :: thesis: verum
end;
hence ex F being Subset of Y st
( F is closed & (A \/ B) /\ F = D ) ; :: thesis: verum
end;
hence A \/ B is discrete ; :: thesis: verum