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:1, 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;

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;
B /\ Q is open by A4, A7;
then A8: A /\ q in the topology of T by A1;
A "/\" q <> Bottom (InclPoset the topology of T) by A2, A5, A6;
then B /\ Q <> {} by A1, A2, A8, YELLOW_1:9;
hence B meets Q ; :: thesis: verum

end;

then B is dense by TOPS_1:45;
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 by A3;
B is open by A1, A3;
then B /\ V is open by A11;
then A12: B /\ V in the topology of T ;
B meets V by A2, A9, A10, A11, TOPS_1:45;
then B /\ V <> {} ;
hence A "/\" v <> Bottom (InclPoset the topology of T) by A1, A2, A12, YELLOW_1:9; :: thesis: verum