:: FINTOPO2 semantic presentation  Show TPTP formulae Show IDV graph for whole article:: Showing IDV graph ... (Click the Palm Trees again to close it)

theorem :: FINTOPO2:1  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for A, B being Subset of FT st A c= B holds
A ^i c= B ^i
proof end;

theorem Th2: :: FINTOPO2:2  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for A being Subset of FT holds A ^delta = (A ^b ) /\ ((A ^i ) ` )
proof end;

theorem :: FINTOPO2:3  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for A being Subset of FT holds A ^delta = (A ^b ) \ (A ^i )
proof end;

theorem :: FINTOPO2:4  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for A being Subset of FT st A ` is open holds
A is closed
proof end;

theorem :: FINTOPO2:5  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for A being Subset of FT st A ` is closed holds
A is open
proof end;

definition
let FT be non empty FT_Space_Str ;
let x, y be Element of FT;
let A be Subset of FT;
func P_1 x,y,A -> Element of BOOLEAN equals :Def1: :: FINTOPO2:def 1
TRUE if ( y in U_FT x & y in A )
otherwise FALSE ;
correctness
coherence
( ( y in U_FT x & y in A implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ) implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def1 defines P_1 FINTOPO2:def 1 :
for FT being non empty FT_Space_Str
for x, y being Element of FT
for A being Subset of FT holds
( ( y in U_FT x & y in A implies P_1 x,y,A = TRUE ) & ( ( not y in U_FT x or not y in A ) implies P_1 x,y,A = FALSE ) );

definition
let FT be non empty FT_Space_Str ;
let x, y be Element of FT;
let A be Subset of FT;
func P_2 x,y,A -> Element of BOOLEAN equals :Def2: :: FINTOPO2:def 2
TRUE if ( y in U_FT x & y in A ` )
otherwise FALSE ;
correctness
coherence
( ( y in U_FT x & y in A ` implies TRUE is Element of BOOLEAN ) & ( ( not y in U_FT x or not y in A ` ) implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def2 defines P_2 FINTOPO2:def 2 :
for FT being non empty FT_Space_Str
for x, y being Element of FT
for A being Subset of FT holds
( ( y in U_FT x & y in A ` implies P_2 x,y,A = TRUE ) & ( ( not y in U_FT x or not y in A ` ) implies P_2 x,y,A = FALSE ) );

theorem :: FINTOPO2:6  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x, y being Element of FT
for A being Subset of FT holds
( P_1 x,y,A = TRUE iff ( y in U_FT x & y in A ) ) by Def1, MARGREL1:38;

theorem :: FINTOPO2:7  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x, y being Element of FT
for A being Subset of FT holds
( P_2 x,y,A = TRUE iff ( y in U_FT x & y in A ` ) ) by Def2, MARGREL1:38;

theorem Th8: :: FINTOPO2:8  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^delta iff ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) )
proof end;

definition
let FT be non empty FT_Space_Str ;
let x, y be Element of FT;
func P_0 x,y -> Element of BOOLEAN equals :Def3: :: FINTOPO2:def 3
TRUE if y in U_FT x
otherwise FALSE ;
correctness
coherence
( ( y in U_FT x implies TRUE is Element of BOOLEAN ) & ( not y in U_FT x implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def3 defines P_0 FINTOPO2:def 3 :
for FT being non empty FT_Space_Str
for x, y being Element of FT holds
( ( y in U_FT x implies P_0 x,y = TRUE ) & ( not y in U_FT x implies P_0 x,y = FALSE ) );

theorem :: FINTOPO2:9  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x, y being Element of FT holds
( P_0 x,y = TRUE iff y in U_FT x ) by Def3, MARGREL1:38;

theorem :: FINTOPO2:10  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^i iff for y being Element of FT st P_0 x,y = TRUE holds
P_1 x,y,A = TRUE )
proof end;

theorem :: FINTOPO2:11  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^b iff ex y1 being Element of FT st P_1 x,y1,A = TRUE )
proof end;

definition
let FT be non empty FT_Space_Str ;
let x be Element of FT;
let A be Subset of FT;
func P_A x,A -> Element of BOOLEAN equals :Def4: :: FINTOPO2:def 4
TRUE if x in A
otherwise FALSE ;
correctness
coherence
( ( x in A implies TRUE is Element of BOOLEAN ) & ( not x in A implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def4 defines P_A FINTOPO2:def 4 :
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( ( x in A implies P_A x,A = TRUE ) & ( not x in A implies P_A x,A = FALSE ) );

theorem :: FINTOPO2:12  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( P_A x,A = TRUE iff x in A ) by Def4, MARGREL1:38;

theorem :: FINTOPO2:13  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^deltai iff ( ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = TRUE ) )
proof end;

theorem :: FINTOPO2:14  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^deltao iff ( ex y1, y2 being Element of FT st
( P_1 x,y1,A = TRUE & P_2 x,y2,A = TRUE ) & P_A x,A = FALSE ) )
proof end;

definition
let FT be non empty FT_Space_Str ;
let x, y be Element of FT;
func P_e x,y -> Element of BOOLEAN equals :Def5: :: FINTOPO2:def 5
TRUE if x = y
otherwise FALSE ;
correctness
coherence
( ( x = y implies TRUE is Element of BOOLEAN ) & ( not x = y implies FALSE is Element of BOOLEAN ) )
;
consistency
for b1 being Element of BOOLEAN holds verum
;
;
end;

:: deftheorem Def5 defines P_e FINTOPO2:def 5 :
for FT being non empty FT_Space_Str
for x, y being Element of FT holds
( ( x = y implies P_e x,y = TRUE ) & ( not x = y implies P_e x,y = FALSE ) );

theorem :: FINTOPO2:15  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x, y being Element of FT holds
( P_e x,y = TRUE iff x = y ) by Def5, MARGREL1:38;

theorem :: FINTOPO2:16  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^s iff ( P_A x,A = TRUE & ( for y being Element of FT holds
( not P_1 x,y,A = TRUE or not P_e x,y = FALSE ) ) ) )
proof end;

theorem :: FINTOPO2:17  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^n iff ( P_A x,A = TRUE & ex y being Element of FT st
( P_1 x,y,A = TRUE & P_e x,y = FALSE ) ) )
proof end;

theorem :: FINTOPO2:18  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FT being non empty FT_Space_Str
for x being Element of FT
for A being Subset of FT holds
( x in A ^f iff ex y being Element of FT st
( P_A y,A = TRUE & P_0 y,x = TRUE ) )
proof end;

definition
attr c1 is strict;
struct FMT_Space_Str -> 1-sorted ;
aggr FMT_Space_Str(# carrier, BNbd #) -> FMT_Space_Str ;
sel BNbd c1 -> Function of the carrier of c1, bool (bool the carrier of c1);
end;

registration
cluster non empty strict FMT_Space_Str ;
existence
ex b1 being FMT_Space_Str st
( not b1 is empty & b1 is strict )
proof end;
end;

definition
let FMT be non empty FMT_Space_Str ;
let x be Element of FMT;
func U_FMT x -> Subset-Family of FMT equals :: FINTOPO2:def 6
the BNbd of FMT . x;
correctness
coherence
the BNbd of FMT . x is Subset-Family of FMT
;
;
end;

:: deftheorem defines U_FMT FINTOPO2:def 6 :
for FMT being non empty FMT_Space_Str
for x being Element of FMT holds U_FMT x = the BNbd of FMT . x;

definition
let T be non empty TopStruct ;
func NeighSp T -> non empty strict FMT_Space_Str means :: FINTOPO2:def 7
( the carrier of it = the carrier of T & ( for x being Point of it holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) );
existence
ex b1 being non empty strict FMT_Space_Str st
( the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) )
proof end;
uniqueness
for b1, b2 being non empty strict FMT_Space_Str st the carrier of b1 = the carrier of T & ( for x being Point of b1 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) & the carrier of b2 = the carrier of T & ( for x being Point of b2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) holds
b1 = b2
proof end;
end;

:: deftheorem defines NeighSp FINTOPO2:def 7 :
for T being non empty TopStruct
for b2 being non empty strict FMT_Space_Str holds
( b2 = NeighSp T iff ( the carrier of b2 = the carrier of T & ( for x being Point of b2 holds U_FMT x = { V where V is Subset of T : ( V in the topology of T & x in V ) } ) ) );

definition
let IT be non empty FMT_Space_Str ;
attr IT is Fo_filled means :Def8: :: FINTOPO2:def 8
for x being Element of IT
for D being Subset of IT st D in U_FMT x holds
x in D;
end;

:: deftheorem Def8 defines Fo_filled FINTOPO2:def 8 :
for IT being non empty FMT_Space_Str holds
( IT is Fo_filled iff for x being Element of IT
for D being Subset of IT st D in U_FMT x holds
x in D );

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fodelta -> Subset of FMT equals :: FINTOPO2:def 9
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` )
}
;
coherence
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` )
}
is Subset of FMT
proof end;
end;

:: deftheorem defines ^Fodelta FINTOPO2:def 9 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` )
}
;

theorem :: FINTOPO2:19  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
canceled;

theorem Th20: :: FINTOPO2:20  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fodelta iff for W being Subset of FMT st W in U_FMT x holds
( W meets A & W meets A ` ) )
proof end;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fob -> Subset of FMT equals :: FINTOPO2:def 10
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A
}
;
coherence
{ x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A
}
is Subset of FMT
proof end;
end;

:: deftheorem defines ^Fob FINTOPO2:def 10 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fob = { x where x is Element of FMT : for W being Subset of FMT st W in U_FMT x holds
W meets A
}
;

theorem Th21: :: FINTOPO2:21  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fob iff for W being Subset of FMT st W in U_FMT x holds
W meets A )
proof end;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Foi -> Subset of FMT equals :: FINTOPO2:def 11
{ x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A )
}
;
coherence
{ x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A )
}
is Subset of FMT
proof end;
end;

:: deftheorem defines ^Foi FINTOPO2:def 11 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Foi = { x where x is Element of FMT : ex V being Subset of FMT st
( V in U_FMT x & V c= A )
}
;

theorem Th22: :: FINTOPO2:22  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Foi iff ex V being Subset of FMT st
( V in U_FMT x & V c= A ) )
proof end;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fos -> Subset of FMT equals :: FINTOPO2:def 12
{ x where x is Element of FMT : ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) )
}
;
coherence
{ x where x is Element of FMT : ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) )
}
is Subset of FMT
proof end;
end;

:: deftheorem defines ^Fos FINTOPO2:def 12 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fos = { x where x is Element of FMT : ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) )
}
;

theorem Th23: :: FINTOPO2:23  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & ex V being Subset of FMT st
( V in U_FMT x & V \ {x} misses A ) ) )
proof end;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fon -> Subset of FMT equals :: FINTOPO2:def 13
A \ (A ^Fos );
coherence
A \ (A ^Fos ) is Subset of FMT
;
end;

:: deftheorem defines ^Fon FINTOPO2:def 13 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fon = A \ (A ^Fos );

theorem :: FINTOPO2:24  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fon iff ( x in A & ( for V being Subset of FMT st V in U_FMT x holds
V \ {x} meets A ) ) )
proof end;

theorem Th25: :: FINTOPO2:25  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st A c= B holds
A ^Fob c= B ^Fob
proof end;

theorem Th26: :: FINTOPO2:26  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st A c= B holds
A ^Foi c= B ^Foi
proof end;

theorem Th27: :: FINTOPO2:27  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A ^Fob ) \/ (B ^Fob ) c= (A \/ B) ^Fob
proof end;

theorem :: FINTOPO2:28  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A /\ B) ^Fob c= (A ^Fob ) /\ (B ^Fob )
proof end;

theorem :: FINTOPO2:29  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A ^Foi ) \/ (B ^Foi ) c= (A \/ B) ^Foi
proof end;

theorem Th30: :: FINTOPO2:30  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT holds (A /\ B) ^Foi c= (A ^Foi ) /\ (B ^Foi )
proof end;

theorem :: FINTOPO2:31  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str holds
( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A \/ B) ^Fob = (A ^Fob ) \/ (B ^Fob ) )
proof end;

theorem :: FINTOPO2:32  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str holds
( ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) iff for A, B being Subset of FMT holds (A ^Foi ) /\ (B ^Foi ) = (A /\ B) ^Foi )
proof end;

theorem :: FINTOPO2:33  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st ( for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 ) ) holds
(A \/ B) ^Fodelta c= (A ^Fodelta ) \/ (B ^Fodelta )
proof end;

theorem :: FINTOPO2:34  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str st FMT is Fo_filled & ( for A, B being Subset of FMT holds (A \/ B) ^Fodelta = (A ^Fodelta ) \/ (B ^Fodelta ) ) holds
for x being Element of FMT
for V1, V2 being Subset of FMT st V1 in U_FMT x & V2 in U_FMT x holds
ex W being Subset of FMT st
( W in U_FMT x & W c= V1 /\ V2 )
proof end;

theorem :: FINTOPO2:35  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for x being Element of FMT
for A being Subset of FMT holds
( x in A ^Fos iff ( x in A & not x in (A \ {x}) ^Fob ) )
proof end;

theorem Th36: :: FINTOPO2:36  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str holds
( FMT is Fo_filled iff for A being Subset of FMT holds A c= A ^Fob )
proof end;

theorem Th37: :: FINTOPO2:37  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str holds
( FMT is Fo_filled iff for A being Subset of FMT holds A ^Foi c= A )
proof end;

theorem Th38: :: FINTOPO2:38  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds ((A ` ) ^Fob ) ` = A ^Foi
proof end;

theorem Th39: :: FINTOPO2:39  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds ((A ` ) ^Foi ) ` = A ^Fob
proof end;

theorem Th40: :: FINTOPO2:40  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob ) /\ ((A ` ) ^Fob )
proof end;

theorem :: FINTOPO2:41  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob ) /\ ((A ^Foi ) ` )
proof end;

theorem :: FINTOPO2:42  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ` ) ^Fodelta
proof end;

theorem :: FINTOPO2:43  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fob ) \ (A ^Foi )
proof end;

definition
let FMT be non empty FMT_Space_Str ;
let A be Subset of FMT;
func A ^Fodel_i -> Subset of FMT equals :: FINTOPO2:def 14
A /\ (A ^Fodelta );
coherence
A /\ (A ^Fodelta ) is Subset of FMT
;
func A ^Fodel_o -> Subset of FMT equals :: FINTOPO2:def 15
(A ` ) /\ (A ^Fodelta );
coherence
(A ` ) /\ (A ^Fodelta ) is Subset of FMT
;
end;

:: deftheorem defines ^Fodel_i FINTOPO2:def 14 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodel_i = A /\ (A ^Fodelta );

:: deftheorem defines ^Fodel_o FINTOPO2:def 15 :
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodel_o = (A ` ) /\ (A ^Fodelta );

theorem :: FINTOPO2:44  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT holds A ^Fodelta = (A ^Fodel_i ) \/ (A ^Fodel_o )
proof end;

definition
let FMT be non empty FMT_Space_Str ;
let G be Subset of FMT;
attr G is Fo_open means :Def16: :: FINTOPO2:def 16
G = G ^Foi ;
attr G is Fo_closed means :Def17: :: FINTOPO2:def 17
G = G ^Fob ;
end;

:: deftheorem Def16 defines Fo_open FINTOPO2:def 16 :
for FMT being non empty FMT_Space_Str
for G being Subset of FMT holds
( G is Fo_open iff G = G ^Foi );

:: deftheorem Def17 defines Fo_closed FINTOPO2:def 17 :
for FMT being non empty FMT_Space_Str
for G being Subset of FMT holds
( G is Fo_closed iff G = G ^Fob );

theorem :: FINTOPO2:45  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT st A ` is Fo_open holds
A is Fo_closed
proof end;

theorem :: FINTOPO2:46  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A being Subset of FMT st A ` is Fo_closed holds
A is Fo_open
proof end;

theorem :: FINTOPO2:47  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A /\ B) ^Fob = (A ^Fob ) /\ (B ^Fob )
proof end;

theorem :: FINTOPO2:48  Show TPTP formulae Show IDV graph:: Showing IDV graph ... (Click the Palm Tree again to close it) Show TPTP problem
for FMT being non empty FMT_Space_Str
for A, B being Subset of FMT st FMT is Fo_filled & ( for x being Element of FMT holds {x} in U_FMT x ) holds
(A ^Foi ) \/ (B ^Foi ) = (A \/ B) ^Foi
proof end;