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;

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

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
B is everywhere_dense
; :: thesis: 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

hence B is everywhere_dense by A4, TOPS_3:36; :: thesis: verum

end;for Q being Subset of T st Q <> {} & Q is open holds

B meets Q

proof

then
B is dense
by TOPS_1:45;
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;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

hence B is everywhere_dense by A4, TOPS_3:36; :: thesis: verum

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