let X be non empty TopSpace; :: thesis: for X0 being SubSpace of X
for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let X0 be SubSpace of X; :: thesis: for C, A being Subset of X
for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let C, A be Subset of X; :: thesis: for B being Subset of X0 st C c= the carrier of X0 & A c= C & A = B holds
( ( C is dense & B is dense ) iff A is dense )
let B be Subset of X0; :: thesis: ( C c= the carrier of X0 & A c= C & A = B implies ( ( C is dense & B is dense ) iff A is dense ) )
assume A1: C c= the carrier of X0 ; :: thesis: ( not A c= C or not A = B or ( ( C is dense & B is dense ) iff A is dense ) )
reconsider P = the carrier of X0 as Subset of X by TSEP_1:1;
assume A2: A c= C ; :: thesis: ( not A = B or ( ( C is dense & B is dense ) iff A is dense ) )
assume A3: A = B ; :: thesis: ( ( C is dense & B is dense ) iff A is dense )
thus ( C is dense & B is dense implies A is dense ) :: thesis: ( A is dense implies ( C is dense & B is dense ) )
proof
assume C is dense ; :: thesis: ( not B is dense or A is dense )
then Cl C = [#] X ;
then A4: [#] X c= Cl P by A1, PRE_TOPC:19;
assume B is dense ; :: thesis: A is dense
then Cl B = [#] X0 ;
then P = (Cl A) /\ ([#] X0) by A3, PRE_TOPC:17;
then Cl P c= Cl (Cl A) by PRE_TOPC:19, XBOOLE_1:17;
then [#] X c= Cl A by A4, XBOOLE_1:1;
then Cl A = [#] X ;
hence A is dense ; :: thesis: verum
end;
thus ( A is dense implies ( C is dense & B is dense ) ) by A2, A3, Th59, TOPS_1:44; :: thesis: verum