let g be set ; :: thesis: ( g in SIMPLEGRAPHS F1() implies P1[g] )
assume A4: g in SIMPLEGRAPHS F1() ; :: thesis: P1[g]
then A5: ex v being finite Subset of F1() ex e being finite Subset of (TWOELEMENTSETS v) st g = SimpleGraphStruct(# v,e #) ;
then reconsider G = g as SimpleGraph of F1() by A4, Def4;
A6: the carrier of G c= F1() by Th18;
per cases ( F1() is empty or not F1() is empty ) ;
suppose A7: F1() is empty ; :: thesis: P1[g]
then the SEdges of G is Subset of {} by A6, Th11;
hence P1[g] by A1, A6, A7; :: thesis: verum
end;
suppose not F1() is empty ; :: thesis: P1[g]
then reconsider X = F1() as non empty set ;
defpred S1[ set ] means P1[ SimpleGraphStruct(# $1,({} (TWOELEMENTSETS $1)) #)];
A8: now :: thesis: for B9 being Element of Fin X
for b being Element of X st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let B9 be Element of Fin X; :: thesis: for b being Element of X st S1[B9] & not b in B9 holds
S1[B9 \/ {b}]
let b be Element of X; :: thesis: ( S1[B9] & not b in B9 implies S1[B9 \/ {b}] )
set g = SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #);
B9 is finite Subset of X by FINSUB_1:16;
then A9: SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #) in SIMPLEGRAPHS F1() ;
then reconsider g = SimpleGraphStruct(# B9,({} (TWOELEMENTSETS B9)) #) as SimpleGraph of F1() by Def4;
assume ( S1[B9] & not b in B9 ) ; :: thesis: S1[B9 \/ {b}]
then P1[ SimpleGraphStruct(# ( the carrier of g \/ {b}),({} (TWOELEMENTSETS ( the carrier of g \/ {b}))) #)] by A2, A9;
hence S1[B9 \/ {b}] ; :: thesis: verum
end;
A10: S1[ {}. X] by A1;
A11: for VV being Element of Fin X holds S1[VV] from SETWISEO:sch 2(A10, A8);
A12: now :: thesis: for VV being Element of Fin X
for EEa being Element of Fin (TWOELEMENTSETS VV)
for EE being Subset of (TWOELEMENTSETS VV) st EEa = EE holds
P1[ SimpleGraphStruct(# VV,EE #)]
let VV be Element of Fin X; :: thesis: for EEa being Element of Fin (TWOELEMENTSETS EEa)
for EE being Subset of (TWOELEMENTSETS EEa) st EE = b3 holds
P1[ SimpleGraphStruct(# EEa,b3 #)]
per cases ( TWOELEMENTSETS VV = {} or TWOELEMENTSETS VV <> {} ) ;
suppose A13: TWOELEMENTSETS VV = {} ; :: thesis: for EEa being Element of Fin (TWOELEMENTSETS EEa)
for EE being Subset of (TWOELEMENTSETS EEa) st EE = b3 holds
P1[ SimpleGraphStruct(# EEa,b3 #)]
let EEa be Element of Fin (TWOELEMENTSETS VV); :: thesis: for EE being Subset of (TWOELEMENTSETS VV) st EEa = EE holds
P1[ SimpleGraphStruct(# VV,EE #)]
let EE be Subset of (TWOELEMENTSETS VV); :: thesis: ( EEa = EE implies P1[ SimpleGraphStruct(# VV,EE #)] )
assume EEa = EE ; :: thesis: P1[ SimpleGraphStruct(# VV,EE #)]
EE = {} (TWOELEMENTSETS VV) by A13;
hence P1[ SimpleGraphStruct(# VV,EE #)] by A11; :: thesis: verum
end;
suppose TWOELEMENTSETS VV <> {} ; :: thesis: for EE being Element of Fin (TWOELEMENTSETS EE)
for EE9 being Subset of (TWOELEMENTSETS EE) st b3 = EE9 holds
P1[ SimpleGraphStruct(# EE,b3 #)]
then reconsider TT = TWOELEMENTSETS VV as non empty set ;
defpred S2[ Element of Fin TT] means for EE being Subset of (TWOELEMENTSETS VV) st EE = $1 holds
P1[ SimpleGraphStruct(# VV,EE #)];
A14: now :: thesis: for ee being Element of Fin TT
for vv being Element of TT st S2[ee] & not vv in ee holds
S2[ee \/ {.vv.}]
let ee be Element of Fin TT; :: thesis: for vv being Element of TT st S2[ee] & not vv in ee holds
S2[ee \/ {.vv.}]
let vv be Element of TT; :: thesis: ( S2[ee] & not vv in ee implies S2[ee \/ {.vv.}] )
assume that
A15: S2[ee] and
A16: not vv in ee ; :: thesis: S2[ee \/ {.vv.}]
reconsider ee9 = ee as Subset of (TWOELEMENTSETS VV) by FINSUB_1:16;
set g = SimpleGraphStruct(# VV,ee9 #);
VV is finite Subset of F1() by FINSUB_1:16;
then SimpleGraphStruct(# VV,ee9 #) is Element of SIMPLEGRAPHS F1() by Th17;
then reconsider g = SimpleGraphStruct(# VV,ee9 #) as SimpleGraph of F1() by Def4;
ex sege being Subset of (TWOELEMENTSETS the carrier of g) st
( sege = the SEdges of g \/ {vv} & P1[ SimpleGraphStruct(# the carrier of g,sege #)] ) by A3, A16, A15;
hence S2[ee \/ {.vv.}] ; :: thesis: verum
end;
A17: S2[ {}. TT]
proof
let EE be Subset of (TWOELEMENTSETS VV); :: thesis: ( EE = {}. TT implies P1[ SimpleGraphStruct(# VV,EE #)] )
assume EE = {}. TT ; :: thesis: P1[ SimpleGraphStruct(# VV,EE #)]
then EE = {} (TWOELEMENTSETS VV) ;
hence P1[ SimpleGraphStruct(# VV,EE #)] by A11; :: thesis: verum
end;
for EE being Element of Fin TT holds S2[EE] from SETWISEO:sch 2(A17, A14);
hence for EE being Element of Fin (TWOELEMENTSETS VV)
for EE9 being Subset of (TWOELEMENTSETS VV) st EE9 = EE holds
P1[ SimpleGraphStruct(# VV,EE9 #)] ; :: thesis: verum
end;
end;
end;
( the carrier of G is Element of Fin X & the SEdges of G is Element of Fin (TWOELEMENTSETS the carrier of G) ) by A5, FINSUB_1:def 5;
hence P1[g] by A12; :: thesis: verum
end;
end;