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:20
.= (Cl ((K /\ L) `)) ` by XBOOLE_1:54 ;
hence (Int K) /\ (Int L) = Int (K /\ L) ; :: thesis: verum