set G1 = the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct;
set G2 = the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct));
take the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) ; :: thesis: ( the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [Graph-like] & the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [Weighted] & the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [ELabeled] & the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [VLabeled] & the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [Ordered] )
thus ( the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [Graph-like] & the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [Weighted] & the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [ELabeled] & the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [VLabeled] & the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct .set (OrderingSelector, the Enumeration of (the_Vertices_of the [Graph-like] [Weighted] [ELabeled] [VLabeled] GraphStruct)) is [Ordered] ) ; :: thesis: verum