let T be non empty TopSpace; for A being Element of (InclPoset the topology of T)
for B being Subset of T st A = B holds
( A is dense iff B is everywhere_dense )
let A be Element of (InclPoset the topology of T); for B being Subset of T st A = B holds
( A is dense iff B is everywhere_dense )
let B be Subset of T; ( A = B implies ( A is dense iff B is everywhere_dense ) )
assume A1:
A = B
; ( A is dense iff B is everywhere_dense )
A2:
Bottom (InclPoset the topology of T) = {}
by PRE_TOPC:5, YELLOW_1:13;
A3:
the carrier of (InclPoset the topology of T) = the topology of T
by YELLOW_1:1;
then A4:
B is open
by A1, PRE_TOPC:def 5;
hereby ( B is everywhere_dense implies A is dense )
assume A5:
A is
dense
;
B is everywhere_dense
for
Q being
Subset of
T st
Q <> {} &
Q is
open holds
B meets Q
proof
let Q be
Subset of
T;
( Q <> {} & Q is open implies B meets Q )
assume that A6:
Q <> {}
and A7:
Q is
open
;
B meets Q
reconsider q =
Q as
Element of
(InclPoset the topology of T) by A3, A7, PRE_TOPC:def 5;
B /\ Q is
open
by A4, A7, TOPS_1:38;
then A8:
A /\ q in the
topology of
T
by A1, PRE_TOPC:def 5;
A "/\" q <> Bottom (InclPoset the topology of T)
by A2, A5, A6, Def4;
then
B /\ Q <> {}
by A1, A2, A8, YELLOW_1:9;
hence
B meets Q
by XBOOLE_0:def 7;
verum
end; then
B is
dense
by TOPS_1:80;
hence
B is
everywhere_dense
by A4, TOPS_3:36;
verum
end;
assume
B is everywhere_dense
; A is dense
then A9:
B is dense
by TOPS_3:33;
let v be Element of (InclPoset the topology of T); WAYBEL12:def 4 ( v <> Bottom (InclPoset the topology of T) implies A "/\" v <> Bottom (InclPoset the topology of T) )
assume A10:
v <> Bottom (InclPoset the topology of T)
; A "/\" v <> Bottom (InclPoset the topology of T)
v in the topology of T
by A3;
then reconsider V = v as Subset of T ;
A11:
V is open
by A3, PRE_TOPC:def 5;
B is open
by A1, A3, PRE_TOPC:def 5;
then
B /\ V is open
by A11, TOPS_1:38;
then A12:
B /\ V in the topology of T
by PRE_TOPC:def 5;
B meets V
by A2, A9, A10, A11, TOPS_1:80;
then
B /\ V <> {}
by XBOOLE_0:def 7;
hence
A "/\" v <> Bottom (InclPoset the topology of T)
by A1, A2, A12, YELLOW_1:9; verum