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

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

end;

hence GSq is real-weighted ; :: thesis:

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

end;

hence GSq is real-elabeled ; :: thesis:

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

end;

hence GSq is real-vlabeled ; :: thesis: