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;
hereby :: thesis: ( B ` is irreducible implies A is irreducible )
assume A4: A is irreducible ; :: thesis: B ` is irreducible
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 b1, b2 being Element of bool the carrier of T holds
( not b1 is closed or not b2 is closed or not B ` = b1 \/ b2 or b1 = B ` or b2 = B ` ) ) )
(B `) ` is open by A1, A3;
hence B ` is closed ; :: thesis: for b1, b2 being Element of bool the carrier of T holds
( not b1 is closed or not b2 is closed or not B ` = b1 \/ b2 or b1 = B ` or b2 = 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;
end;
thus ( B ` is irreducible implies A is irreducible ) by A1, Th40; :: thesis: verum