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[ object ] 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_4 & e = y `2_4 & s = y `3_4 & t = y `4_4 & M = MultiGraphStruct(# v,e,s,t #) & M is Subgraph of G );
consider X being set such that
A1: for x being object 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[ object , object ] 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_4 & e = y `2_4 & s = y `3_4 & t = y `4_4 & M = MultiGraphStruct(# v,e,s,t #) & M is Subgraph of G & $2 = M );
A2: for a, b, c being object st S2[a,b] & S2[a,c] holds
b = c ;
consider Y being set such that
A3: for z being object holds
( z in Y iff ex x being object st
( x in X & S2[x,z] ) ) from TARSKI:sch 1(A2);
 take Y ; :: thesis: for x being object holds
( x in Y iff x is strict Subgraph of G )
let x be object ; :: 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 object 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 object 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] )
A4: ( the carrier of H c= V & the carrier' of H c= the carrier' of G ) by Def18;
( the Source of H in PFuncs ( the carrier' of G,V) & the Target of H in PFuncs ( the carrier' of G,V) ) by Lm4;
then reconsider y9 = y as Element of [:(bool V),(bool the carrier' of G),(PFuncs ( the carrier' of G,V)),(PFuncs ( the carrier' of G,V)):] by A4, MCART_1:80;
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 ;
A5: ( v = y9 `1_4 & the carrier' of H = y9 `2_4 ) by MCART_1:def 8, MCART_1:def 9;
A6: ( s = y9 `3_4 & t = y9 `4_4 ) by MCART_1:def 10, MCART_1:def 11;
hence y in X by A1, A5; :: thesis: S2[y,x]
thus S2[y,x] by A5, A6; :: thesis: verum
end;
hence x in Y by A3; :: thesis: verum