defpred S1[ set , set ] means for SX being SimplicialComplexStr of X st the topology of SX = $1 & [#] SX = [#] KX holds
the topology of (subdivision (P,SX)) = $2;
set BBK = bool (bool ([#] KX));
A1: for x being set st x in bool (bool ([#] KX)) holds
ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] )
proof
let x be set ; :: thesis: ( x in bool (bool ([#] KX)) implies ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] ) )
assume A2: x in bool (bool ([#] KX)) ; :: thesis: ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] )
per cases ( ex SX being SimplicialComplexStr of X st
( the topology of SX = x & [#] SX = [#] KX ) or for SX being SimplicialComplexStr of X holds
( the topology of SX <> x or [#] SX <> [#] KX ) ) ;
suppose ex SX being SimplicialComplexStr of X st
( the topology of SX = x & [#] SX = [#] KX ) ; :: thesis: ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] )
then consider SX being SimplicialComplexStr of X such that
A3: the topology of SX = x and
A4: [#] SX = [#] KX ;
take T = the topology of (subdivision (P,SX)); :: thesis: ( T in bool (bool ([#] KX)) & S1[x,T] )
[#] (subdivision (P,SX)) = [#] SX by Def20;
hence T in bool (bool ([#] KX)) by A4; :: thesis: S1[x,T]
let SX1 be SimplicialComplexStr of X; :: thesis: ( the topology of SX1 = x & [#] SX1 = [#] KX implies the topology of (subdivision (P,SX1)) = T )
assume A5: ( the topology of SX1 = x & [#] SX1 = [#] KX ) ; :: thesis: the topology of (subdivision (P,SX1)) = T
TopStruct(# the carrier of SX, the topology of SX #) = TopStruct(# the carrier of SX1, the topology of SX1 #) by A3, A4, A5;
hence the topology of (subdivision (P,SX1)) = T by Th60; :: thesis: verum
end;
suppose A6: for SX being SimplicialComplexStr of X holds
( the topology of SX <> x or [#] SX <> [#] KX ) ; :: thesis: ex y being set st
( y in bool (bool ([#] KX)) & S1[x,y] )
take x ; :: thesis: ( x in bool (bool ([#] KX)) & S1[x,x] )
thus ( x in bool (bool ([#] KX)) & S1[x,x] ) by A2, A6; :: thesis: verum
end;
end;
end;
consider f being Function of (bool (bool ([#] KX))),(bool (bool ([#] KX))) such that
A7: for x being set st x in bool (bool ([#] KX)) holds
S1[x,f . x] from FUNCT_2:sch 1(A1);
 deffunc H1( set , set ) -> set = f . $2;
consider g being Function such that
A8: ( dom g = NAT & g . 0 = the topology of KX & ( for n being Nat holds g . (n + 1) = H1(n,g . n) ) ) from NAT_1:sch 11();
 defpred S2[ Nat] means ( ex SX being SimplicialComplexStr of X st
( the topology of SX = g . $1 & [#] SX = [#] KX & ( $1 > 0 implies SX is strict ) ) & ( for SX being SimplicialComplexStr of X st the topology of SX = g . $1 & [#] SX = [#] KX holds
g . ($1 + 1) = the topology of (subdivision (P,SX)) ) );
g . (0 + 1) = f . the topology of KX by A8;
then A9: g . 1 = the topology of (subdivision (P,KX)) by A7;
A10: S2[ 0 ]
proof
thus ex SX being SimplicialComplexStr of X st
( the topology of SX = g . 0 & [#] SX = [#] KX & ( 0 > 0 implies SX is strict ) ) by A8; :: thesis: for SX being SimplicialComplexStr of X st the topology of SX = g . 0 & [#] SX = [#] KX holds
g . (0 + 1) = the topology of (subdivision (P,SX))
let SX be SimplicialComplexStr of X; :: thesis: ( the topology of SX = g . 0 & [#] SX = [#] KX implies g . (0 + 1) = the topology of (subdivision (P,SX)) )
assume ( the topology of SX = g . 0 & [#] SX = [#] KX ) ; :: thesis: g . (0 + 1) = the topology of (subdivision (P,SX))
then TopStruct(# the carrier of SX, the topology of SX #) = TopStruct(# the carrier of KX, the topology of KX #) by A8;
hence g . (0 + 1) = the topology of (subdivision (P,SX)) by A9, Th60; :: thesis: verum
end;
defpred S3[ set , set ] means for k being Nat st k = $1 holds
( ( k = 0 implies $2 = KX ) & ( k > 0 implies for SF being Subset-Family of KX st SF = g . k holds
$2 = TopStruct(# the carrier of KX,SF #) ) );
A11: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
set k1 = k + 1;
given SX being SimplicialComplexStr of X such that A12: the topology of SX = g . k and
A13: [#] SX = [#] KX and
( k > 0 implies SX is strict ) ; :: thesis: ( ex SX being SimplicialComplexStr of X st
( the topology of SX = g . k & [#] SX = [#] KX & not g . (k + 1) = the topology of (subdivision (P,SX)) ) or S2[k + 1] )
assume for SX being SimplicialComplexStr of X st the topology of SX = g . k & [#] SX = [#] KX holds
g . (k + 1) = the topology of (subdivision (P,SX)) ; :: thesis: S2[k + 1]
then A14: g . (k + 1) = the topology of (subdivision (P,SX)) by A12, A13;
[#] (subdivision (P,SX)) = [#] KX by A13, Def20;
hence ex SX being SimplicialComplexStr of X st
( the topology of SX = g . (k + 1) & [#] SX = [#] KX & ( k + 1 > 0 implies SX is strict ) ) by A14; :: thesis: for SX being SimplicialComplexStr of X st the topology of SX = g . (k + 1) & [#] SX = [#] KX holds
g . ((k + 1) + 1) = the topology of (subdivision (P,SX))
let S1 be SimplicialComplexStr of X; :: thesis: ( the topology of S1 = g . (k + 1) & [#] S1 = [#] KX implies g . ((k + 1) + 1) = the topology of (subdivision (P,S1)) )
assume A15: ( the topology of S1 = g . (k + 1) & [#] S1 = [#] KX ) ; :: thesis: g . ((k + 1) + 1) = the topology of (subdivision (P,S1))
g . ((k + 1) + 1) = f . (g . (k + 1)) by A8;
hence g . ((k + 1) + 1) = the topology of (subdivision (P,S1)) by A7, A15; :: thesis: verum
end;
A16: for k being Nat holds S2[k] from NAT_1:sch 2(A10, A11);
 A17: for x being set st x in NAT holds
ex y being set st S3[x,y]
proof
let x be set ; :: thesis: ( x in NAT implies ex y being set st S3[x,y] )
assume x in NAT ; :: thesis: ex y being set st S3[x,y]
then reconsider m = x as Nat ;
per cases ( m = 0 or m > 0 ) ;
suppose A18: m = 0 ; :: thesis: ex y being set st S3[x,y]
take KX ; :: thesis: S3[x,KX]
thus S3[x,KX] by A18; :: thesis: verum
end;
suppose A19: m > 0 ; :: thesis: ex y being set st S3[x,y]
consider K1 being SimplicialComplexStr of X such that
A20: the topology of K1 = g . m and
A21: [#] K1 = [#] KX and
( m > 0 implies K1 is strict ) by A16;
reconsider TOP = the topology of K1 as Subset-Family of KX by A21;
take TopStruct(# the carrier of KX,TOP #) ; :: thesis: S3[x, TopStruct(# the carrier of KX,TOP #)]
thus S3[x, TopStruct(# the carrier of KX,TOP #)] by A19, A20; :: thesis: verum
end;
end;
end;
consider h being Function such that
A22: ( dom h = NAT & ( for x being set st x in NAT holds
S3[x,h . x] ) ) from CLASSES1:sch 1(A17);
 A23: 0 in NAT by ORDINAL1:def 12;
then A24: h . 0 = KX by A22;
A25: for k being Nat
for K1 being SimplicialComplexStr of X st h . k = K1 holds
h . (k + 1) = subdivision (P,K1)
proof
let k be Nat; :: thesis: for K1 being SimplicialComplexStr of X st h . k = K1 holds
h . (k + 1) = subdivision (P,K1)
let KK be SimplicialComplexStr of X; :: thesis: ( h . k = KK implies h . (k + 1) = subdivision (P,KK) )
assume A26: h . k = KK ; :: thesis: h . (k + 1) = subdivision (P,KK)
S2[k + 1] by A16;
then consider K1 being SimplicialComplexStr of X such that
A27: the topology of K1 = g . (k + 1) and
A28: [#] K1 = [#] KX ;
reconsider TOP1 = the topology of K1 as Subset-Family of KX by A28;
A29: k in NAT by ORDINAL1:def 12;
S2[k] by A16;
then consider K2 being SimplicialComplexStr of X such that
A30: the topology of K2 = g . k and
A31: [#] K2 = [#] KX ;
reconsider TOP2 = the topology of K2 as Subset-Family of KX by A31;
A32: [#] (subdivision (P,KK)) = [#] KK by Def20;
per cases ( k = 0 or k > 0 ) ;
suppose A33: k = 0 ; :: thesis: h . (k + 1) = subdivision (P,KK)
then TOP1 = the topology of (subdivision (P,KK)) by A8, A10, A24, A26, A27;
hence h . (k + 1) = subdivision (P,KK) by A22, A24, A26, A27, A32, A33; :: thesis: verum
end;
suppose k > 0 ; :: thesis: h . (k + 1) = subdivision (P,KK)
then A34: KK = TopStruct(# the carrier of KX,TOP2 #) by A22, A26, A29, A30;
then [#] KK = [#] KX ;
then g . (k + 1) = the topology of (subdivision (P,KK)) by A16, A30, A34;
hence h . (k + 1) = subdivision (P,KK) by A22, A32, A34; :: thesis: verum
end;
end;
end;
per cases ( n = 0 or n > 0 ) ;
suppose A35: n = 0 ; :: thesis: ex b1 being SimplicialComplexStr of X ex F being Function st
( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
take KX ; :: thesis: ex F being Function st
( F . 0 = KX & F . n = KX & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
thus ex F being Function st
( F . 0 = KX & F . n = KX & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) ) by A22, A24, A25, A35; :: thesis: verum
end;
suppose A36: n > 0 ; :: thesis: ex b1 being SimplicialComplexStr of X ex F being Function st
( F . 0 = KX & F . n = b1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
consider K1 being SimplicialComplexStr of X such that
A37: the topology of K1 = g . n and
A38: [#] K1 = [#] KX and
A39: ( n > 0 implies K1 is strict ) by A16;
reconsider K1 = K1 as strict SimplicialComplexStr of X by A36, A39;
take K1 ; :: thesis: ex F being Function st
( F . 0 = KX & F . n = K1 & dom F = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = F . k holds
F . (k + 1) = subdivision (P,KX1) ) )
take h ; :: thesis: ( h . 0 = KX & h . n = K1 & dom h = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = h . k holds
h . (k + 1) = subdivision (P,KX1) ) )
thus h . 0 = KX by A22, A23; :: thesis: ( h . n = K1 & dom h = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = h . k holds
h . (k + 1) = subdivision (P,KX1) ) )
n in NAT by ORDINAL1:def 12;
hence ( h . n = K1 & dom h = NAT & ( for k being Nat
for KX1 being SimplicialComplexStr of X st KX1 = h . k holds
h . (k + 1) = subdivision (P,KX1) ) ) by A22, A25, A36, A37, A38; :: thesis: verum
end;
end;