let T be non empty TopSpace; :: thesis: 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); :: thesis: for B being Subset of T st A = B holds
( A is dense iff B is everywhere_dense )
let B be Subset of T; :: thesis: ( A = B implies ( A is dense iff B is everywhere_dense ) )
assume A1: A = B ; :: thesis: ( 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;
A4: B is open

proof

thus B in the topology of T by A1, A3; :: according to PRE_TOPC:def 5 :: thesis: verum

end;

hereby :: thesis: ( B is everywhere_dense implies A is dense )

assume A5: A is dense ; :: thesis: 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; :: thesis: ( Q <> {} & Q is open implies B meets Q )
assume that
A6: Q <> {} and
A7: Q is open ; :: thesis: B meets Q
reconsider q = Q as Element of (InclPoset the topology of T) by A3, A7, PRE_TOPC:def 5;
A8: A "/\" q <> Bottom (InclPoset the topology of T) by A2, A5, A6, Def4;
B /\ Q is open by A4, A7, TOPS_1:38;
then A /\ q in the topology of T by A1, PRE_TOPC:def 5;
then B /\ Q <> {} by A1, A2, A8, YELLOW_1:9;
hence B meets Q by XBOOLE_0:def 7; :: thesis: verum

end;

then B is dense by TOPS_1:80;
hence B is everywhere_dense by A4, TOPS_3:36; :: thesis: verum

end;

assume B is everywhere_dense ; :: thesis: A is dense
then A9: B is dense by TOPS_3:33;
let v be Element of (InclPoset the topology of T); :: according to WAYBEL12:def 4 :: thesis: ( 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) ; :: thesis: 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

proof

thus V in the topology of T by A3; :: according to PRE_TOPC:def 5 :: thesis: verum

end;

then B meets V by A2, A9, A10, TOPS_1:80;
then A12: B /\ V <> {} by XBOOLE_0:def 7;
B is open

proof

thus B in the topology of T by A1, A3; :: according to PRE_TOPC:def 5 :: thesis: verum

end;

then B /\ V is open by A11, TOPS_1:38;
then B /\ V in the topology of T by PRE_TOPC:def 5;
hence A "/\" v <> Bottom (InclPoset the topology of T) by A1, A2, A12, YELLOW_1:9; :: thesis: verum