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

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