:: deftheorem defines real-WEV GLIB_003:def 31 :
for GSq being WEVGraphSeq holds
( GSq is real-WEV iff for x being Nat holds GSq . x is real-WEV );