for G being set st G in SIMPLEGRAPHS F₁() holds
P₁[G]

A1: P₁[ SimpleGraphStruct(# {},({} (TWOELEMENTSETS {})) #)] and
A2: for g being SimpleGraph of F₁()
for v being set st g in SIMPLEGRAPHS F₁() & P₁[g] & v in F₁() & not v in the carrier of g holds
P₁[ SimpleGraphStruct(# ( the carrier of g \/ {v}),({} (TWOELEMENTSETS ( the carrier of g \/ {v}))) #)] and
A3: for g being SimpleGraph of F₁()
for e being set st P₁[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} & P₁[ SimpleGraphStruct(# the carrier of g,sege #)] )