let X, OTHER be set ; ( OTHER is_SetOfSimpleGraphs_of X implies SIMPLEGRAPHS X c= OTHER )
defpred S1[ set ] means $1 in OTHER;
assume A1:
OTHER is_SetOfSimpleGraphs_of X
; SIMPLEGRAPHS X c= OTHER
A2:
for g being SimpleGraph of X
for v being set st g in SIMPLEGRAPHS X & S1[g] & v in X & not v in the carrier of g holds
S1[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)]
A4:
for g being SimpleGraph of X
for e being set st S1[g] & e in TWOELEMENTSETS the carrier of g & not e in the SEdges of g holds
ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )
proof
let g be
SimpleGraph of
X;
for e being set st S1[g] & e in TWOELEMENTSETS the carrier of g & not e in the SEdges of g holds
ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )let e be
set ;
( S1[g] & e in TWOELEMENTSETS the carrier of g & not e in the SEdges of g implies ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] ) )
assume that A5:
g in OTHER
and A6:
e in TWOELEMENTSETS the
carrier of
g
and A7:
not
e in the
SEdges of
g
;
ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,sege #)] )
set SVg = the
carrier of
g;
set SEg = the
SEdges of
g;
consider v1,
v2 being
object such that A8:
(
v1 in the
carrier of
g &
v2 in the
carrier of
g &
v1 <> v2 )
and A9:
e = {v1,v2}
by A6, Th8;
the
carrier of
g is
finite Subset of
X
by Th21;
then consider v1v2 being
finite Subset of
(TWOELEMENTSETS the carrier of g) such that A10:
(
v1v2 = the
SEdges of
g \/ {{v1,v2}} &
SimpleGraphStruct(# the
carrier of
g,
v1v2 #)
in OTHER )
by A1, A5, A7, A8, A9;
take
v1v2
;
( v1v2 = the SEdges of g \/ {e} & S1[ SimpleGraphStruct(# the carrier of g,v1v2 #)] )
thus
(
v1v2 = the
SEdges of
g \/ {e} &
S1[
SimpleGraphStruct(# the
carrier of
g,
v1v2 #)] )
by A9, A10;
verum
end;
let e be object ; TARSKI:def 3 ( not e in SIMPLEGRAPHS X or e in OTHER )
assume A11:
e in SIMPLEGRAPHS X
; e in OTHER
A12:
S1[ SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #)]
by A1;
for e being set st e in SIMPLEGRAPHS X holds
S1[e]
from SGRAPH1:sch 1(A12, A2, A4);
hence
e in OTHER
by A11; verum