let T be non empty TopSpace; :: thesis: for A being Element of (InclPoset the topology of T)

for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds

( A is irreducible iff B ` is irreducible )

let A be Element of (InclPoset the topology of T); :: thesis: for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds

( A is irreducible iff B ` is irreducible )

let B be Subset of T; :: thesis: ( A = B & A <> Top (InclPoset the topology of T) implies ( A is irreducible iff B ` is irreducible ) )

assume that

A1: A = B and

A2: A <> Top (InclPoset the topology of T) ; :: thesis: ( A is irreducible iff B ` is irreducible )

A3: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;

for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds

( A is irreducible iff B ` is irreducible )

let A be Element of (InclPoset the topology of T); :: thesis: for B being Subset of T st A = B & A <> Top (InclPoset the topology of T) holds

( A is irreducible iff B ` is irreducible )

let B be Subset of T; :: thesis: ( A = B & A <> Top (InclPoset the topology of T) implies ( A is irreducible iff B ` is irreducible ) )

assume that

A1: A = B and

A2: A <> Top (InclPoset the topology of T) ; :: thesis: ( A is irreducible iff B ` is irreducible )

A3: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;

hereby :: thesis: ( B ` is irreducible implies A is irreducible )

thus
( B ` is irreducible implies A is irreducible )
by A1, Th40; :: thesis: verumassume A4:
A is irreducible
; :: thesis: B ` is irreducible

thus B ` is irreducible :: thesis: verum

end;thus B ` is irreducible :: thesis: verum

proof

B <> the carrier of T
by A1, A2, YELLOW_1:24;

then the carrier of T \ B <> {} by XBOOLE_1:37;

hence not B ` is empty ; :: according to YELLOW_8:def 3 :: thesis: ( B ` is closed & ( for b_{1}, b_{2} being Element of bool the carrier of T holds

( not b_{1} is closed or not b_{2} is closed or not B ` = b_{1} \/ b_{2} or b_{1} = B ` or b_{2} = B ` ) ) )

(B `) ` is open by A1, A3;

hence B ` is closed ; :: thesis: for b_{1}, b_{2} being Element of bool the carrier of T holds

( not b_{1} is closed or not b_{2} is closed or not B ` = b_{1} \/ b_{2} or b_{1} = B ` or b_{2} = B ` )

let S1, S2 be Subset of T; :: thesis: ( not S1 is closed or not S2 is closed or not B ` = S1 \/ S2 or S1 = B ` or S2 = B ` )

assume that

A5: ( S1 is closed & S2 is closed ) and

A6: B ` = S1 \/ S2 ; :: thesis: ( S1 = B ` or S2 = B ` )

A7: ( S1 ` is open & S2 ` is open ) by A5;

then reconsider s1 = S1 ` , s2 = S2 ` as Element of (InclPoset the topology of T) by A3;

(S1 `) /\ (S2 `) is open by A7;

then A8: s1 /\ s2 in the topology of T ;

B = (S1 \/ S2) ` by A6

.= (S1 `) /\ (S2 `) by XBOOLE_1:53 ;

then A = s1 "/\" s2 by A1, A8, YELLOW_1:9;

then ( A = s1 or A = s2 ) by A4;

hence ( S1 = B ` or S2 = B ` ) by A1; :: thesis: verum

end;then the carrier of T \ B <> {} by XBOOLE_1:37;

hence not B ` is empty ; :: according to YELLOW_8:def 3 :: thesis: ( B ` is closed & ( for b

( not b

(B `) ` is open by A1, A3;

hence B ` is closed ; :: thesis: for b

( not b

let S1, S2 be Subset of T; :: thesis: ( not S1 is closed or not S2 is closed or not B ` = S1 \/ S2 or S1 = B ` or S2 = B ` )

assume that

A5: ( S1 is closed & S2 is closed ) and

A6: B ` = S1 \/ S2 ; :: thesis: ( S1 = B ` or S2 = B ` )

A7: ( S1 ` is open & S2 ` is open ) by A5;

then reconsider s1 = S1 ` , s2 = S2 ` as Element of (InclPoset the topology of T) by A3;

(S1 `) /\ (S2 `) is open by A7;

then A8: s1 /\ s2 in the topology of T ;

B = (S1 \/ S2) ` by A6

.= (S1 `) /\ (S2 `) by XBOOLE_1:53 ;

then A = s1 "/\" s2 by A1, A8, YELLOW_1:9;

then ( A = s1 or A = s2 ) by A4;

hence ( S1 = B ` or S2 = B ` ) by A1; :: thesis: verum