let GSq be [Weighted] [ELabeled] [VLabeled] GraphSeq; :: thesis: ( GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled implies GSq is real-WEV )
assume A2: ( GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled ) ; :: thesis: GSq is real-WEV
let x be Nat; :: according to GLIB_003:def 31 :: thesis: GSq . x is real-WEV
reconsider G = GSq . x as real-weighted real-elabeled real-vlabeled WEVGraph by A2;
G is real-WEV ;
hence GSq . x is real-WEV ; :: thesis: verum