reconsider V = the carrier of G as non empty set ;
set E = the carrier' of G;
set Prod = [:(bool V),(bool the carrier' of G),(PFuncs the carrier' of G,V),(PFuncs the carrier' of G,V):];
defpred S1[ set ] means ex y being Element of [:(bool V),(bool the carrier' of G),(PFuncs the carrier' of G,V),(PFuncs the carrier' of G,V):] ex M being Graph ex v being non empty set ex e being set ex s, t being Function of e,v st
( y = $1 & v = y `1 & e = y `2 & s = y `3 & t = y `4 & M = MultiGraphStruct(# v,e,s,t #) & M is Subgraph of G );
consider X being set such that
A1: for x being set holds
( x in X iff ( x in [:(bool V),(bool the carrier' of G),(PFuncs the carrier' of G,V),(PFuncs the carrier' of G,V):] & S1[x] ) ) from XBOOLE_0:sch 1();
 defpred S2[ set , set ] means ex y being Element of [:(bool V),(bool the carrier' of G),(PFuncs the carrier' of G,V),(PFuncs the carrier' of G,V):] ex M being strict Graph ex v being non empty set ex e being set ex s, t being Function of e,v st
( y = $1 & v = y `1 & e = y `2 & s = y `3 & t = y `4 & M = MultiGraphStruct(# v,e,s,t #) & M is Subgraph of G & $2 = M );
A2: for a, b, c being set st S2[a,b] & S2[a,c] holds
b = c ;
consider Y being set such that
A3: for z being set holds
( z in Y iff ex x being set st
( x in X & S2[x,z] ) ) from TARSKI:sch 1(A2);
 take Y ; :: thesis: for x being set holds
( x in Y iff x is strict Subgraph of G )
let x be set ; :: thesis: ( x in Y iff x is strict Subgraph of G )
thus ( x in Y implies x is strict Subgraph of G ) :: thesis: ( x is strict Subgraph of G implies x in Y )
proof
assume x in Y ; :: thesis: x is strict Subgraph of G
then ex z being set st
( z in X & S2[z,x] ) by A3;
hence x is strict Subgraph of G ; :: thesis: verum
end;
assume x is strict Subgraph of G ; :: thesis: x in Y
then reconsider H = x as strict Subgraph of G ;
ex y being set st
( y in X & S2[y,x] )
proof
take y = [the carrier of H,the carrier' of H,the Source of H,the Target of H]; :: thesis: ( y in X & S2[y,x] )
y in [:(bool V),(bool the carrier' of G),(PFuncs the carrier' of G,V),(PFuncs the carrier' of G,V):]
proof
A4: the carrier of H c= V by Def17;
A5: the carrier' of H c= the carrier' of G by Def17;
( the Source of H in PFuncs the carrier' of G,V & the Target of H in PFuncs the carrier' of G,V ) by Lm9;
hence y in [:(bool V),(bool the carrier' of G),(PFuncs the carrier' of G,V),(PFuncs the carrier' of G,V):] by A4, A5, MCART_1:84; :: thesis: verum
end;
then reconsider y' = y as Element of [:(bool V),(bool the carrier' of G),(PFuncs the carrier' of G,V),(PFuncs the carrier' of G,V):] ;
reconsider v = the carrier of H as non empty set ;
set e = the carrier' of H;
reconsider s = the Source of H as Function of the carrier' of H,v ;
reconsider t = the Target of H as Function of the carrier' of H,v ;
A6: ( v = y' `1 & the carrier' of H = y' `2 & s = y' `3 & t = y' `4 ) by MCART_1:59;
hence y in X by A1; :: thesis: S2[y,x]
thus S2[y,x] by A6; :: thesis: verum
end;
hence x in Y by A3; :: thesis: verum