let T be non empty TopSpace; :: thesis: for A, B being Subset of T
for G being Rain of A,B
for p being Point of T holds Rainbow (p,G) c= DYADIC
let A, B be Subset of T; :: thesis: for G being Rain of A,B
for p being Point of T holds Rainbow (p,G) c= DYADIC
let G be Rain of A,B; :: thesis: for p being Point of T holds Rainbow (p,G) c= DYADIC
let p be Point of T; :: thesis: Rainbow (p,G) c= DYADIC
for x being set st x in Rainbow (p,G) holds
x in DYADIC by Def5;
hence Rainbow (p,G) c= DYADIC by TARSKI:def 3; :: thesis: verum