set V = meet (the_Vertices_of S);
set E = meet (the_Edges_of S);
reconsider s = meet (the_Source_of S) as Function ;
( dom s = meet (the_Edges_of S) & rng s c= meet (the_Vertices_of S) ) by PARTFUN1:def 2, RELAT_1:def 19;
then reconsider s = s as Function of (meet (the_Edges_of S)),(meet (the_Vertices_of S)) by FUNCT_2:2;
reconsider t = meet (the_Target_of S) as Function ;
( dom t = meet (the_Edges_of S) & rng t c= meet (the_Vertices_of S) ) by PARTFUN1:def 2, RELAT_1:def 19;
then reconsider t = t as Function of (meet (the_Edges_of S)),(meet (the_Vertices_of S)) by FUNCT_2:2;
take createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t) ; :: thesis: ( the_Vertices_of (createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t)) = meet (the_Vertices_of S) & the_Edges_of (createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t)) = meet (the_Edges_of S) & the_Source_of (createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t)) = meet (the_Source_of S) & the_Target_of (createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t)) = meet (the_Target_of S) )
thus ( the_Vertices_of (createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t)) = meet (the_Vertices_of S) & the_Edges_of (createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t)) = meet (the_Edges_of S) & the_Source_of (createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t)) = meet (the_Source_of S) & the_Target_of (createGraph ((meet (the_Vertices_of S)),(meet (the_Edges_of S)),s,t)) = meet (the_Target_of S) ) ; :: thesis: verum