let GSq be [Weighted] [ELabeled] [VLabeled] GraphSeq; :: thesis: ( GSq is real-WEV implies ( GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled ) )
assume A1: for x being Nat holds GSq . x is real-WEV ; :: according to GLIB_003:def 31 :: thesis: ( GSq is real-weighted & GSq is real-elabeled & GSq is real-vlabeled )

now :: thesis: for x being Nat holds GSq . x is real-weighted

let x be Nat; :: thesis: GSq . x is real-weighted
reconsider G = GSq . x as real-WEV WEVGraph by A1;
G is real-WEV ;
hence GSq . x is real-weighted ; :: thesis: verum

end;

hence GSq is real-weighted ; :: thesis: ( GSq is real-elabeled & GSq is real-vlabeled )

now :: thesis: for x being Nat holds GSq . x is real-elabeled

let x be Nat; :: thesis: GSq . x is real-elabeled
reconsider G = GSq . x as real-WEV WEVGraph by A1;
G is real-WEV ;
hence GSq . x is real-elabeled ; :: thesis: verum

end;

hence GSq is real-elabeled ; :: thesis: GSq is real-vlabeled

now :: thesis: for x being Nat holds GSq . x is real-vlabeled

let x be Nat; :: thesis: GSq . x is real-vlabeled
reconsider G = GSq . x as real-WEV WEVGraph by A1;
G is real-WEV ;
hence GSq . x is real-vlabeled ; :: thesis: verum

end;

hence GSq is real-vlabeled ; :: thesis: verum