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 & B ` is irreducible holds

A is irreducible

let A be Element of (InclPoset the topology of T); :: thesis: for B being Subset of T st A = B & B ` is irreducible holds

A is irreducible

let B be Subset of T; :: thesis: ( A = B & B ` is irreducible implies A is irreducible )

assume A1: A = B ; :: thesis: ( not B ` is irreducible or A is irreducible )

assume that

( not B ` is empty & B ` is closed ) and

A2: for S1, S2 being Subset of T st S1 is closed & S2 is closed & B ` = S1 \/ S2 & not S1 = B ` holds

S2 = B ` ; :: according to YELLOW_8:def 3 :: thesis: A is irreducible

let x, y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def 2 :: thesis: ( not A = x "/\" y or x = A or y = A )

assume A3: A = x "/\" y ; :: thesis: ( x = A or y = A )

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

then ( x in the topology of T & y in the topology of T ) ;

then reconsider x1 = x, y1 = y as Subset of T ;

A5: y1 is open by A4;

then A6: y1 ` is closed ;

A7: x1 is open by A4;

then x1 /\ y1 is open by A5;

then x /\ y in the topology of T ;

then A = x /\ y by A3, YELLOW_1:9;

then A8: B ` = (x1 `) \/ (y1 `) by A1, XBOOLE_1:54;

x1 ` is closed by A7;

then ( x1 ` = B ` or y1 ` = B ` ) by A2, A6, A8;

hence ( x = A or y = A ) by A1, TOPS_1:1; :: thesis: verum

for B being Subset of T st A = B & B ` is irreducible holds

A is irreducible

let A be Element of (InclPoset the topology of T); :: thesis: for B being Subset of T st A = B & B ` is irreducible holds

A is irreducible

let B be Subset of T; :: thesis: ( A = B & B ` is irreducible implies A is irreducible )

assume A1: A = B ; :: thesis: ( not B ` is irreducible or A is irreducible )

assume that

( not B ` is empty & B ` is closed ) and

A2: for S1, S2 being Subset of T st S1 is closed & S2 is closed & B ` = S1 \/ S2 & not S1 = B ` holds

S2 = B ` ; :: according to YELLOW_8:def 3 :: thesis: A is irreducible

let x, y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def 2 :: thesis: ( not A = x "/\" y or x = A or y = A )

assume A3: A = x "/\" y ; :: thesis: ( x = A or y = A )

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

then ( x in the topology of T & y in the topology of T ) ;

then reconsider x1 = x, y1 = y as Subset of T ;

A5: y1 is open by A4;

then A6: y1 ` is closed ;

A7: x1 is open by A4;

then x1 /\ y1 is open by A5;

then x /\ y in the topology of T ;

then A = x /\ y by A3, YELLOW_1:9;

then A8: B ` = (x1 `) \/ (y1 `) by A1, XBOOLE_1:54;

x1 ` is closed by A7;

then ( x1 ` = B ` or y1 ` = B ` ) by A2, A6, A8;

hence ( x = A or y = A ) by A1, TOPS_1:1; :: thesis: verum