let T be TopSpace; :: thesis: for A being Subset of T st A is 1st_class holds

( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) )

let A be Subset of T; :: thesis: ( A is 1st_class implies ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) )

Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;

then A1: Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19;

Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;

then A2: Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19;

assume A is 1st_class ; :: thesis: ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) )

then A3: Int (Cl A) c= Cl (Int A) ;

then A4: Cl (Int (Cl A)) c= Cl (Cl (Int A)) by PRE_TOPC:19;

Int (Int (Cl A)) c= Int (Cl (Int A)) by A3, TOPS_1:19;

hence ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) by A1, A4, A2, XBOOLE_0:def 10; :: thesis: verum

( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) )

let A be Subset of T; :: thesis: ( A is 1st_class implies ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) )

Cl (Int A) c= Cl A by PRE_TOPC:19, TOPS_1:16;

then A1: Int (Cl (Int A)) c= Int (Cl A) by TOPS_1:19;

Int A c= Int (Cl A) by PRE_TOPC:18, TOPS_1:19;

then A2: Cl (Int A) c= Cl (Int (Cl A)) by PRE_TOPC:19;

assume A is 1st_class ; :: thesis: ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) )

then A3: Int (Cl A) c= Cl (Int A) ;

then A4: Cl (Int (Cl A)) c= Cl (Cl (Int A)) by PRE_TOPC:19;

Int (Int (Cl A)) c= Int (Cl (Int A)) by A3, TOPS_1:19;

hence ( Int (Cl A) = Int (Cl (Int A)) & Cl (Int A) = Cl (Int (Cl A)) ) by A1, A4, A2, XBOOLE_0:def 10; :: thesis: verum