set C = the non empty set ;
set f = the closure Function of (bool the non empty set ),(bool the non empty set );
set g = the interior Function of (bool the non empty set ),(bool the non empty set );
take TwoOpStruct(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ), the interior Function of (bool the non empty set ),(bool the non empty set ) #) ; :: thesis: ( TwoOpStruct(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ), the interior Function of (bool the non empty set ),(bool the non empty set ) #) is with_closure & TwoOpStruct(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ), the interior Function of (bool the non empty set ),(bool the non empty set ) #) is with_interior )
thus ( TwoOpStruct(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ), the interior Function of (bool the non empty set ),(bool the non empty set ) #) is with_closure & TwoOpStruct(# the non empty set , the closure Function of (bool the non empty set ),(bool the non empty set ), the interior Function of (bool the non empty set ),(bool the non empty set ) #) is with_interior ) ; :: thesis: verum