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

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