let g be set ; :: thesis: ( g in SIMPLEGRAPHS F₁() implies P₁[g] )
assume A4: g in SIMPLEGRAPHS F₁() ; :: thesis: P₁[g]
then consider v being finite Subset of F₁(), e being finite Subset of (TWOELEMENTSETS v) such that
A5: g = SimpleGraphStruct(# v,e #) ;
reconsider G = g as SimpleGraph of F₁() by A4, A5, Def7;
A6: ( the carrier of G c= F₁() & the SEdges of G c= TWOELEMENTSETS the carrier of G ) by Th23;

per cases ( F₁() is empty or not F₁() is empty ) ;

suppose A7: F₁() is empty ; :: thesis: P₁[g]

then the SEdges of G is Subset of {} by A6, Th13;
hence P₁[g] by A1, A6, A7; :: thesis: verum

end;

suppose not F₁() is empty ; :: thesis: P₁[g]

then reconsider X = F₁() as non empty set ;
defpred S₁[ set ] means P₁[ SimpleGraphStruct(# $1,({} (TWOELEMENTSETS $1)) #)];
A8: S₁[ {}. X] by A1;

A9: now

let B' be Element of Fin X; :: thesis: for b being Element of X st S₁[B'] & not b in B' holds
S₁[B' \/ {b}]
let b be Element of X; :: thesis: ( S₁[B'] & not b in B' implies S₁[B' \/ {b}] )
assume A10: ( S₁[B'] & not b in B' ) ; :: thesis: S₁[B' \/ {b}]
set g = SimpleGraphStruct(# B',({} (TWOELEMENTSETS B')) #);
B' is finite Subset of X by FINSUB_1:32;
then A11: SimpleGraphStruct(# B',({} (TWOELEMENTSETS B')) #) in SIMPLEGRAPHS F₁() ;
then reconsider g = SimpleGraphStruct(# B',({} (TWOELEMENTSETS B')) #) as SimpleGraph of F₁() by Def7;
P₁[ SimpleGraphStruct(# (the carrier of g \/ {b}),({} (TWOELEMENTSETS (the carrier of g \/ {b}))) #)] by A2, A10, A11;
hence S₁[B' \/ {b}] ; :: thesis: verum

end;

A12: for VV being Element of Fin X holds S₁[VV] from SETWISEO:sch 2(A8, A9);

A13: now

let VV be Element of Fin X; :: thesis: for EEa being Finite_Subset of (TWOELEMENTSETS EEa)
for EE being Subset of (TWOELEMENTSETS EEa) st EE = b₃ holds
P₁[ SimpleGraphStruct(# EEa,b₃ #)]

per cases ( TWOELEMENTSETS VV = {} or TWOELEMENTSETS VV <> {} ) ;

suppose A14: TWOELEMENTSETS VV = {} ; :: thesis: for EEa being Finite_Subset of (TWOELEMENTSETS EEa)
for EE being Subset of (TWOELEMENTSETS EEa) st EE = b₃ holds
P₁[ SimpleGraphStruct(# EEa,b₃ #)]

let EEa be Finite_Subset of (TWOELEMENTSETS VV); :: thesis: for EE being Subset of (TWOELEMENTSETS VV) st EEa = EE holds
P₁[ SimpleGraphStruct(# VV,EE #)]
let EE be Subset of (TWOELEMENTSETS VV); :: thesis: ( EEa = EE implies P₁[ SimpleGraphStruct(# VV,EE #)] )
assume EEa = EE ; :: thesis: P₁[ SimpleGraphStruct(# VV,EE #)]
EE = {} (TWOELEMENTSETS VV) by A14;
hence P₁[ SimpleGraphStruct(# VV,EE #)] by A12; :: thesis: verum

end;

suppose TWOELEMENTSETS VV <> {} ; :: thesis: for EE being Finite_Subset of (TWOELEMENTSETS EE)
for EE' being Subset of (TWOELEMENTSETS EE) st b₃ = EE' holds
P₁[ SimpleGraphStruct(# EE,b₃ #)]

then reconsider TT = TWOELEMENTSETS VV as non empty set ;
defpred S₂[ Finite_Subset of TT] means for EE being Subset of (TWOELEMENTSETS VV) st EE = $1 holds
P₁[ SimpleGraphStruct(# VV,EE #)];
A15: S₂[ {}. TT]

proof

let EE be Subset of (TWOELEMENTSETS VV); :: thesis: ( EE = {}. TT implies P₁[ SimpleGraphStruct(# VV,EE #)] )
assume EE = {}. TT ; :: thesis: P₁[ SimpleGraphStruct(# VV,EE #)]
then EE = {} (TWOELEMENTSETS VV) ;
hence P₁[ SimpleGraphStruct(# VV,EE #)] by A12; :: thesis: verum

end;

A16: now

let ee be Finite_Subset of TT; :: thesis: for vv being Element of TT st S₂[ee] & not vv in ee holds
S₂[ee \/ {.vv.}]
let vv be Element of TT; :: thesis: ( S₂[ee] & not vv in ee implies S₂[ee \/ {.vv.}] )
assume A17: ( S₂[ee] & not vv in ee ) ; :: thesis: S₂[ee \/ {.vv.}]
reconsider ee' = ee as Subset of (TWOELEMENTSETS VV) by FINSUB_1:32;
A18: VV is finite Subset of F₁() by FINSUB_1:32;
set g = SimpleGraphStruct(# VV,ee' #);
SimpleGraphStruct(# VV,ee' #) is Element of SIMPLEGRAPHS F₁() by A18, Th21;
then reconsider g = SimpleGraphStruct(# VV,ee' #) as SimpleGraph of F₁() by Def7;
P₁[g] by A17;
then consider sege being Subset of (TWOELEMENTSETS the carrier of g) such that
A19: sege = the SEdges of g \/ {vv} and
A20: P₁[ SimpleGraphStruct(# the carrier of g,sege #)] by A3, A17;
thus S₂[ee \/ {.vv.}] by A19, A20; :: thesis: verum

end;

for EE being Finite_Subset of TT holds S₂[EE] from SETWISEO:sch 2(A15, A16);
hence for EE being Finite_Subset of (TWOELEMENTSETS VV)
for EE' being Subset of (TWOELEMENTSETS VV) st EE' = EE holds
P₁[ SimpleGraphStruct(# VV,EE' #)] ; :: thesis: verum

end;

end;

end;

A21: the carrier of G is Finite_Subset of X by A5, FINSUB_1:def 5;
the SEdges of G is Finite_Subset of (TWOELEMENTSETS the carrier of G) by A5, FINSUB_1:def 5;
hence P₁[g] by A13, A21; :: thesis: verum

end;

end;