let T be TopSpace; :: thesis: for A, B, C being Subset of T st C is open & A /\ C c= B holds
C c= Int ((A `) \/ B)
let A, B, C be Subset of T; :: thesis: ( C is open & A /\ C c= B implies C c= Int ((A `) \/ B) )
assume that
A1: C is open and
A2: A /\ C c= B ; :: thesis: C c= Int ((A `) \/ B)
A3: C c= C \/ (A `) by XBOOLE_1:7;
(A /\ C) \/ (A `) = (A \/ (A `)) /\ (C \/ (A `)) by XBOOLE_1:24
.= ([#] T) /\ (C \/ (A `)) by PRE_TOPC:2
.= C \/ (A `) by XBOOLE_1:28 ;
then C \/ (A `) c= B \/ (A `) by A2, XBOOLE_1:9;
then C c= B \/ (A `) by A3;
then Int C c= Int ((A `) \/ B) by TOPS_1:19;
hence C c= Int ((A `) \/ B) by A1, TOPS_1:23; :: thesis: verum