let GX be TopStruct ; :: thesis: for T, W being Subset of GX holds (Int T) \/ (Int W) c= Int (T \/ W)
let T, W be Subset of GX; :: thesis: (Int T) \/ (Int W) c= Int (T \/ W)
A1: Cl ((T `) /\ (W `)) c= (Cl (T `)) /\ (Cl (W `)) by PRE_TOPC:21;
(Int T) \/ (Int W) = ((Cl (T `)) /\ (Cl (W `))) ` by XBOOLE_1:54;
then (Int T) \/ (Int W) c= (Cl ((T `) /\ (W `))) ` by A1, SUBSET_1:12;
hence (Int T) \/ (Int W) c= Int (T \/ W) by XBOOLE_1:53; :: thesis: verum