let S be Graph-membered set ; :: thesis: ( card (the_Vertices_of S) c= card S & card (the_Edges_of S) c= card S & card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )
defpred S₁[ object , object ] means ex G being _Graph st
( $1 = G & $2 = the_Vertices_of G );
A1: for x, y1, y2 being object st x in S & S₁[x,y1] & S₁[x,y2] holds
y1 = y2 ;
A2: for x being object st x in S holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis: ( x in S implies ex y being object st S₁[x,y] )
assume x in S ; :: thesis: ex y being object st S₁[x,y]
then reconsider G = x as _Graph ;
take the_Vertices_of G ; :: thesis: S₁[x, the_Vertices_of G]
take G ; :: thesis: ( x = G & the_Vertices_of G = the_Vertices_of G )
thus ( x = G & the_Vertices_of G = the_Vertices_of G ) ; :: thesis: verum

end;

consider f1 being Function such that
A3: ( dom f1 = S & ( for x being object st x in S holds
S₁[x,f1 . x] ) ) from FUNCT_1:sch 2(A1, A2);

now :: thesis: for x being object st x in the_Vertices_of S holds
x in rng f1

let x be object ; :: thesis: ( x in the_Vertices_of S implies x in rng f1 )
assume x in the_Vertices_of S ; :: thesis: x in rng f1
then consider G being _Graph such that
A4: ( G in S & x = the_Vertices_of G ) by Def14;
consider G0 being _Graph such that
A5: ( G = G0 & f1 . G = the_Vertices_of G0 ) by A3, A4;
thus x in rng f1 by A3, A4, A5, FUNCT_1:3; :: thesis: verum

end;

hence card (the_Vertices_of S) c= card S by A3, CARD_1:12, TARSKI:def 3; :: thesis: ( card (the_Edges_of S) c= card S & card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )
defpred S₂[ object , object ] means ex G being _Graph st
( $1 = G & $2 = the_Edges_of G );
A6: for x, y1, y2 being object st x in S & S₂[x,y1] & S₂[x,y2] holds
y1 = y2 ;
A7: for x being object st x in S holds
ex y being object st S₂[x,y]

proof

let x be object ; :: thesis: ( x in S implies ex y being object st S₂[x,y] )
assume x in S ; :: thesis: ex y being object st S₂[x,y]
then reconsider G = x as _Graph ;
take the_Edges_of G ; :: thesis: S₂[x, the_Edges_of G]
take G ; :: thesis: ( x = G & the_Edges_of G = the_Edges_of G )
thus ( x = G & the_Edges_of G = the_Edges_of G ) ; :: thesis: verum

end;

consider f2 being Function such that
A8: ( dom f2 = S & ( for x being object st x in S holds
S₂[x,f2 . x] ) ) from FUNCT_1:sch 2(A6, A7);

now :: thesis: for x being object st x in the_Edges_of S holds
x in rng f2

let x be object ; :: thesis: ( x in the_Edges_of S implies x in rng f2 )
assume x in the_Edges_of S ; :: thesis: x in rng f2
then consider G being _Graph such that
A9: ( G in S & x = the_Edges_of G ) by Def15;
consider G0 being _Graph such that
A10: ( G = G0 & f2 . G = the_Edges_of G0 ) by A8, A9;
thus x in rng f2 by A8, A9, A10, FUNCT_1:3; :: thesis: verum

end;

hence card (the_Edges_of S) c= card S by A8, CARD_1:12, TARSKI:def 3; :: thesis: ( card (the_Source_of S) c= card S & card (the_Target_of S) c= card S )
defpred S₃[ object , object ] means ex G being _Graph st
( $1 = G & $2 = the_Source_of G );
A11: for x, y1, y2 being object st x in S & S₃[x,y1] & S₃[x,y2] holds
y1 = y2 ;
A12: for x being object st x in S holds
ex y being object st S₃[x,y]

proof

let x be object ; :: thesis: ( x in S implies ex y being object st S₃[x,y] )
assume x in S ; :: thesis: ex y being object st S₃[x,y]
then reconsider G = x as _Graph ;
take the_Source_of G ; :: thesis: S₃[x, the_Source_of G]
take G ; :: thesis: ( x = G & the_Source_of G = the_Source_of G )
thus ( x = G & the_Source_of G = the_Source_of G ) ; :: thesis: verum

end;

consider f3 being Function such that
A13: ( dom f3 = S & ( for x being object st x in S holds
S₃[x,f3 . x] ) ) from FUNCT_1:sch 2(A11, A12);

now :: thesis: for x being object st x in the_Source_of S holds
x in rng f3

let x be object ; :: thesis: ( x in the_Source_of S implies x in rng f3 )
assume x in the_Source_of S ; :: thesis: x in rng f3
then consider G being _Graph such that
A14: ( G in S & x = the_Source_of G ) by Def16;
consider G0 being _Graph such that
A15: ( G = G0 & f3 . G = the_Source_of G0 ) by A13, A14;
thus x in rng f3 by A13, A14, A15, FUNCT_1:3; :: thesis: verum

end;

hence card (the_Source_of S) c= card S by A13, CARD_1:12, TARSKI:def 3; :: thesis: card (the_Target_of S) c= card S
defpred S₄[ object , object ] means ex G being _Graph st
( $1 = G & $2 = the_Target_of G );
A16: for x, y1, y2 being object st x in S & S₄[x,y1] & S₄[x,y2] holds
y1 = y2 ;
A17: for x being object st x in S holds
ex y being object st S₄[x,y]

proof

let x be object ; :: thesis: ( x in S implies ex y being object st S₄[x,y] )
assume x in S ; :: thesis: ex y being object st S₄[x,y]
then reconsider G = x as _Graph ;
take the_Target_of G ; :: thesis: S₄[x, the_Target_of G]
take G ; :: thesis: ( x = G & the_Target_of G = the_Target_of G )
thus ( x = G & the_Target_of G = the_Target_of G ) ; :: thesis: verum

end;

consider f4 being Function such that
A18: ( dom f4 = S & ( for x being object st x in S holds
S₄[x,f4 . x] ) ) from FUNCT_1:sch 2(A16, A17);

now :: thesis: for x being object st x in the_Target_of S holds
x in rng f4

let x be object ; :: thesis: ( x in the_Target_of S implies x in rng f4 )
assume x in the_Target_of S ; :: thesis: x in rng f4
then consider G being _Graph such that
A19: ( G in S & x = the_Target_of G ) by Def17;
consider G0 being _Graph such that
A20: ( G = G0 & f4 . G = the_Target_of G0 ) by A18, A19;
thus x in rng f4 by A18, A19, A20, FUNCT_1:3; :: thesis: verum

end;

hence card (the_Target_of S) c= card S by A18, CARD_1:12, TARSKI:def 3; :: thesis: verum