let T be non empty TopSpace; :: thesis: for S being irreducible Subset of T
for V being Element of (InclPoset the topology of T) st V = S ` holds
V is prime
let S be irreducible Subset of T; :: thesis: for V being Element of (InclPoset the topology of T) st V = S ` holds
V is prime
let V be Element of (InclPoset the topology of T); :: thesis: ( V = S ` implies V is prime )
assume A1: V = S ` ; :: thesis: V is prime
set sL = the topology of T;
let X, Y be Element of (InclPoset the topology of T); :: according to WAYBEL_6:def 6 :: thesis: ( not X "/\" Y <= V or X <= V or Y <= V )
A2: 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 X' = X, Y' = Y as Subset of T ;
X' /\ Y' in the topology of T by A2, PRE_TOPC:def 1;
then A3: X /\ Y = X "/\" Y by YELLOW_1:9;
assume X "/\" Y <= V ; :: thesis: ( X <= V or Y <= V )
then X /\ Y c= V by A3, YELLOW_1:3;
then S c= (X' /\ Y') ` by A1, Lm1;
then S c= (X' ` ) \/ (Y' ` ) by XBOOLE_1:54;
then S = ((X' ` ) \/ (Y' ` )) /\ S by XBOOLE_1:28;
then A4: S = ((X' ` ) /\ S) \/ ((Y' ` ) /\ S) by XBOOLE_1:23;
A5: S is closed by YELLOW_8:def 4;
Y' is open by A2, PRE_TOPC:def 5;
then Y' ` is closed by TOPS_1:30;
then A6: (Y' ` ) /\ S is closed by A5, TOPS_1:35;
X' is open by A2, PRE_TOPC:def 5;
then X' ` is closed by TOPS_1:30;
then (X' ` ) /\ S is closed by A5, TOPS_1:35;
then ( S = (X' ` ) /\ S or S = (Y' ` ) /\ S ) by A6, A4, YELLOW_8:def 4;
then ( S c= X' ` or S c= Y' ` ) by XBOOLE_1:17;
then ( X c= V or Y c= V ) by A1, Lm1;
hence ( X <= V or Y <= V ) by YELLOW_1:3; :: thesis: verum