let S, T be non empty TopSpace; :: thesis: for A being irreducible Subset of S
for B being Subset of T st A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) holds
B is irreducible
let A be irreducible Subset of S; :: thesis: for B being Subset of T st A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) holds
B is irreducible
let B be Subset of T; :: thesis: ( A = B & TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) implies B is irreducible )
assume that
A1: A = B and
A2: TopStruct(# the carrier of S,the topology of S #) = TopStruct(# the carrier of T,the topology of T #) ; :: thesis: B is irreducible
( not A is empty & A is closed ) by YELLOW_8:def 4;
hence ( not B is empty & B is closed ) by A1, A2, TOPS_3:79; :: according to YELLOW_8:def 4 :: thesis: for b₁, b₂ being Element of bool the carrier of T holds
( not b₁ is closed or not b₂ is closed or not B = K20((bool the carrier of T),b₁,b₂) or b₁ = B or b₂ = B )
let B1, B2 be Subset of T; :: thesis: ( not B1 is closed or not B2 is closed or not B = K20((bool the carrier of T),B1,B2) or B1 = B or B2 = B )
assume A3: ( B1 is closed & B2 is closed & B = B1 \/ B2 ) ; :: thesis: ( B1 = B or B2 = B )
reconsider A1 = B1, A2 = B2 as Subset of S by A2;
( A1 is closed & A2 is closed & A = A1 \/ A2 ) by A1, A2, A3, TOPS_3:79;
hence ( B1 = B or B2 = B ) by A1, YELLOW_8:def 4; :: thesis: verum