let G be Grating of d; :: thesis: G is V27()
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in Seg d or G . i is finite )
assume i in Seg d ; :: thesis: G . i is finite
hence G . i is finite by Def4; :: thesis: verum