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: (Int T) \/ (Int W) = ((Cl (T ` )) /\ (Cl (W ` ))) ` by XBOOLE_1:54;
Cl ((T ` ) /\ (W ` )) c= (Cl (T ` )) /\ (Cl (W ` )) by PRE_TOPC:51;
then (Int T) \/ (Int W) c= (Cl ((T ` ) /\ (W ` ))) ` by A1, SUBSET_1:31;
hence (Int T) \/ (Int W) c= Int (T \/ W) by XBOOLE_1:53; :: thesis: verum