let X be non empty set ; :: thesis: for X0 being set
for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0
let X0 be set ; :: thesis: for A being proper Subset of (X0 -DiscreteTop X) holds Int A = A /\ X0
let A be proper Subset of (X0 -DiscreteTop X); :: thesis: Int A = A /\ X0
the carrier of (X0 -DiscreteTop X) = X by Def8;
then A1: X <> A by SUBSET_1:def 6;
thus Int A = IFEQ (A,X,A,(A /\ X0)) by Def8
.= A /\ X0 by A1, FUNCOP_1:def 8 ; :: thesis: verum