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, XBOOLE_0:def 7
.= A /\ B ;
then A2: A /\ ((A ` ) \/ B) c= B by XBOOLE_1:17;
A /\ (Int ((A ` ) \/ B)) c= A /\ ((A ` ) \/ B) by TOPS_1:44, XBOOLE_1:26;
hence A /\ (Int ((A ` ) \/ B)) c= B by A2, XBOOLE_1:1; :: thesis: verum