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