let FT1, FT2 be non empty RelStr ; :: thesis: for A being Subset of FT1
for B being Subset of FT2
for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b ) c= B ^b
let A be Subset of FT1; :: thesis: for B being Subset of FT2
for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b ) c= B ^b
let B be Subset of FT2; :: thesis: for f being Function of FT1,FT2 st f is_continuous 0 & B = f .: A holds
f .: (A ^b ) c= B ^b
let f be Function of FT1,FT2; :: thesis: ( f is_continuous 0 & B = f .: A implies f .: (A ^b ) c= B ^b )
assume A1:
( f is_continuous 0 & B = f .: A )
; :: thesis: f .: (A ^b ) c= B ^b
thus
f .: (A ^b ) c= B ^b
:: thesis: verumproof
let y be
set ;
:: according to TARSKI:def 3 :: thesis: ( not y in f .: (A ^b ) or y in B ^b )
assume
y in f .: (A ^b )
;
:: thesis: y in B ^b
then consider x being
set such that A2:
(
x in dom f &
x in A ^b &
y = f . x )
by FUNCT_1:def 12;
reconsider x0 =
x as
Element of
FT1 by A2;
reconsider y0 =
y as
Element of
FT2 by A2, FUNCT_2:7;
consider z being
Element of
FT1 such that A3:
(
z = x &
U_FT z meets A )
by A2;
A4:
(U_FT x0) /\ A <> {}
by A3, XBOOLE_0:def 7;
f .: (U_FT x0,0 ) c= U_FT y0,
0
by A1, A2, Def2;
then
f .: (U_FT x0) c= U_FT y0,
0
by FINTOPO3:47;
then A5:
f .: (U_FT x0) c= U_FT y0
by FINTOPO3:47;
dom f = the
carrier of
FT1
by FUNCT_2:def 1;
then A6:
f .: ((U_FT x0) /\ A) <> {}
by A4, RELAT_1:152;
A7:
f .: ((U_FT x0) /\ A) c= (f .: (U_FT x0)) /\ (f .: A)
by RELAT_1:154;
(f .: (U_FT x0)) /\ (f .: A) c= (U_FT y0) /\ (f .: A)
by A5, XBOOLE_1:26;
then
(U_FT y0) /\ (f .: A) <> {}
by A6, A7;
then
U_FT y0 meets B
by A1, XBOOLE_0:def 7;
hence
y in B ^b
;
:: thesis: verum
end;