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 meet-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 meet-irreducible iff B ` is irreducible )
let B be Subset of T; :: thesis: ( A = B & A <> Top (InclPoset the topology of T) implies ( A is meet-irreducible iff B ` is irreducible ) )
assume that
A1: A = B and
A2: A <> Top (InclPoset the topology of T) ; :: thesis: ( A is meet-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 meet-irreducible )

assume A4: A is meet-irreducible ; :: thesis: B ` is irreducible
thus B ` is irreducible :: thesis: verum

proof

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

now

assume the carrier of T \ B = {} ; :: thesis: contradiction
then the carrier of T c= B by XBOOLE_1:37;
hence contradiction by A5, XBOOLE_0:def 10; :: thesis: verum

end;

hence not B ` is empty ; :: according to YELLOW_8:def 3 :: thesis: ( B ` is closed & ( for b₁, b₂ being Element of bool the carrier of T holds
( not b₁ is closed or not b₂ is closed or not B ` = b<sub>1</sub> \/ b<sub>2</sub> or b<sub>1</sub> = B ` or b₂ = B ` ) ) )
(B `) ` is open by A1, A3, PRE_TOPC:def 2;
hence B ` is closed ; :: thesis: for b₁, b₂ being Element of bool the carrier of T holds
( not b₁ is closed or not b₂ is closed or not B ` = b<sub>1</sub> \/ b<sub>2</sub> or b<sub>1</sub> = B ` or b₂ = 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
A6: ( S1 is closed & S2 is closed ) and
A7: B ` = S1 \/ S2 ; :: thesis: ( S1 = B ` or S2 = B ` )
A8: ( S1 ` is open & S2 ` is open ) by A6;
then reconsider s1 = S1 ` , s2 = S2 ` as Element of (InclPoset the topology of T) by A3, PRE_TOPC:def 2;
(S1 `) /\ (S2 `) is open by A8;
then A9: s1 /\ s2 in the topology of T by PRE_TOPC:def 2;
B = (S1 \/ S2) ` by A7
.= (S1 `) /\ (S2 `) by XBOOLE_1:53 ;
then A = s1 "/\" s2 by A1, A9, YELLOW_1:9;
then ( A = s1 or A = s2 ) by A4, WAYBEL_6:def 2;
hence ( S1 = B ` or S2 = B ` ) by A1; :: thesis: verum

end;

end;

thus ( B ` is irreducible implies A is meet-irreducible ) by A1, Th44; :: thesis: verum