reconsider S = MultiGraphStruct(# the carrier of G,the carrier' of G,the Source of G,the Target of G #) as Graph ;
A1: for v being set st v in the carrier' of S holds
( the Source of S . v = the Source of G . v & the Target of S . v = the Target of G . v & the Source of G . v in the carrier of S & the Target of G . v in the carrier of S ) by FUNCT_2:7;
A2: S is Subgraph of G by A1, Def18;
thus ex b₁ being Subgraph of G st b₁ is strict by A2; :: thesis: verum