let T1 be empty TopSpace; :: thesis: for T2 being TopSpace
for f being Function of T1,T2 holds f is continuous
let T2 be TopSpace; :: thesis: for f being Function of T1,T2 holds f is continuous
let f be Function of T1,T2; :: thesis: f is continuous
let A be Subset of T2; :: according to PRE_TOPC:def 6 :: thesis: ( not A is closed or f " A is closed )
thus ( not A is closed or f " A is closed ) ; :: thesis: verum