reconsider S = MultiGraphStruct(# the carrier of G, the carrier' of G, the Source of G, the Target of G #) as Graph ;
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:5;
then S is Subgraph of G by Def18;
hence ex b₁ being Subgraph of G st b₁ is strict ; :: thesis: verum