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:7;
then S is Subgraph of G by Def17;
hence ex b₁ being Subgraph of G st b₁ is strict ; :: thesis: verum