begin
Lm1:
for A being set
for B, C, D being Subset of A st B \ C = {} holds
B misses D \ C
Lm2:
for A, B, C being set holds (A /\ B) \ C = (A \ C) /\ (B \ C)
Lm3:
for X being TopStruct
for X0 being SubSpace of X holds TopStruct(# the carrier of X0, the topology of X0 #) is strict SubSpace of X
Lm4:
for T being TopStruct holds TopStruct(# the carrier of T, the topology of T #) is SubSpace of T
begin
begin
begin