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