let TS be TopSpace; :: thesis: for K, L being Subset of TS holds (Int K) /\ (Int L) = Int (K /\ L)
let K, L be Subset of TS; :: thesis: (Int K) /\ (Int L) = Int (K /\ L)
(Int K) /\ (Int L) = ((Cl (K ` )) \/ (Cl (L ` ))) ` by XBOOLE_1:53
.= (Cl ((K ` ) \/ (L ` ))) ` by PRE_TOPC:50
.= (Cl ((K /\ L) ` )) ` by XBOOLE_1:54 ;
hence (Int K) /\ (Int L) = Int (K /\ L) ; :: thesis: verum