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
; for x being object holds
( x in Y iff x is strict Subgraph of G )
let x be object ; ( x in Y iff x is strict Subgraph of G )
thus
( x in Y implies x is strict Subgraph of G )
( x is strict Subgraph of G implies x in Y )
assume
x is strict Subgraph of G
; 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];
( 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;
S2[y,x]
thus
S2[
y,
x]
by A5, A6;
verum
end;
hence
x in Y
by A3; verum