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 3;
hence ( not B is empty & B is closed ) by A1, A2, TOPS_3:79; :: according to YELLOW_8:def 3 :: thesis: for b₁, b₂ being Element of K6( the carrier of T) holds
( not b₁ is closed or not b₂ is closed or not B = K20(K6( 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(K6( the carrier of T),B1,B2) or B1 = B or B2 = B )
assume that
A3: ( B1 is closed & B2 is closed ) and
A4: 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 ) by A2, A3, TOPS_3:79;
hence ( B1 = B or B2 = B ) by A1, A4, YELLOW_8:def 3; :: thesis: verum