let T be non empty TopSpace-like TopaddGrStr ; :: thesis: ( ( for a, b being Element of T
for W being a_neighborhood of a + b ex A being a_neighborhood of a ex B being a_neighborhood of b st A + B c= W ) implies T is BinContinuous )
assume A1: for a, b being Element of T
for W being a_neighborhood of a + b ex A being a_neighborhood of a ex B being a_neighborhood of b st A + B c= W ; :: thesis: T is BinContinuous
let f be Function of [:T,T:],T; :: according to GROUP_1A:def 47 :: thesis: ( f = the addF of T implies f is continuous )
assume A2: f = the addF of T ; :: thesis: f is continuous
for W being Point of [:T,T:]
for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G

proof

let W be Point of [:T,T:]; :: thesis: for G being a_neighborhood of f . W ex H being a_neighborhood of W st f .: H c= G
let G be a_neighborhood of f . W; :: thesis: ex H being a_neighborhood of W st f .: H c= G
consider a, b being Point of T such that
A3: W = [a,b] by BORSUK_1:10;
f . W = a + b by A2, A3;
then consider A being a_neighborhood of a, B being a_neighborhood of b such that
A4: A + B c= G by A1;
reconsider H = [:A,B:] as a_neighborhood of W by A3;
take H ; :: thesis: f .: H c= G
thus f .: H c= G by A2, A4, Th14; :: thesis: verum

end;

hence f is continuous by BORSUK_1:def 1; :: thesis: verum