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 meet-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 meet-irreducible
let B be Subset of T; :: thesis: ( A = B & B ` is irreducible implies A is meet-irreducible )
assume A1: A = B ; :: thesis: ( not B ` is irreducible or A is meet-irreducible )
A2: the carrier of (InclPoset the topology of T) = the topology of T by YELLOW_1:1;
assume that
( not B ` is empty & B ` is closed ) and
A3: 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 4 :: thesis: A is meet-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 A4: A = x "/\" y ; :: thesis: ( x = A or y = A )
( x in the topology of T & y in the topology of T ) by A2;
then reconsider x1 = x, y1 = y as Subset of T ;
A5: ( x1 is open & y1 is open ) by A2, PRE_TOPC:def 5;
then A6: ( x1 ` is closed & y1 ` is closed ) by TOPS_1:30;
x1 /\ y1 is open by A5, TOPS_1:38;
then x /\ y in the topology of T by PRE_TOPC:def 5;
then A = x /\ y by A4, YELLOW_1:9;
then B ` = (x1 ` ) \/ (y1 ` ) by A1, XBOOLE_1:54;
then ( x1 ` = B ` or y1 ` = B ` ) by A3, A6;
hence ( x = A or y = A ) by A1, TOPS_1:21; :: thesis: verum