A1: TopStruct(# the carrier of (Omega T), the topology of (Omega T) #) = TopStruct(# the carrier of T, the topology of T #) by Def2;
hence the carrier of (Omega T) in the topology of (Omega T) by PRE_TOPC:def 1; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b₁ being Element of bool (bool the carrier of (Omega T)) holds
( not b₁ c= the topology of (Omega T) or K238( the carrier of (Omega T),b₁) in the topology of (Omega T) ) ) & ( for b₁, b₂ being Element of bool the carrier of (Omega T) holds
( not b₁ in the topology of (Omega T) or not b₂ in the topology of (Omega T) or b₁ /\ b₂ in the topology of (Omega T) ) ) )
thus ( ( for b₁ being Element of bool (bool the carrier of (Omega T)) holds
( not b₁ c= the topology of (Omega T) or K238( the carrier of (Omega T),b₁) in the topology of (Omega T) ) ) & ( for b₁, b₂ being Element of bool the carrier of (Omega T) holds
( not b₁ in the topology of (Omega T) or not b₂ in the topology of (Omega T) or b₁ /\ b₂ in the topology of (Omega T) ) ) ) by A1, PRE_TOPC:def 1; :: thesis: verum