let T be TopSpace; :: thesis: for A, B being Subset of T holds A /\ (Int ((A `) \/ B)) c= B
let A, B be Subset of T; :: thesis: A /\ (Int ((A `) \/ B)) c= B
A1: A misses A ` by XBOOLE_1:79;
A /\ ((A `) \/ B) = (A /\ (A `)) \/ (A /\ B) by XBOOLE_1:23
.= {} \/ (A /\ B) by A1
.= A /\ B ;
then A2: A /\ ((A `) \/ B) c= B by XBOOLE_1:17;
A /\ (Int ((A `) \/ B)) c= A /\ ((A `) \/ B) by TOPS_1:16, XBOOLE_1:26;
hence A /\ (Int ((A `) \/ B)) c= B by A2; :: thesis: verum