let T be non empty TopSpace; 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; 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); ( V = S ` implies V is prime )
assume A1:
V = S `
; V is prime
set sL = the topology of T;
let X, Y be Element of (InclPoset the topology of T); WAYBEL_6:def 6 ( 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 X9 = X, Y9 = Y as Subset of T ;
X9 /\ Y9 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
; ( X <= V or Y <= V )
then
X /\ Y c= V
by A3, YELLOW_1:3;
then
S c= (X9 /\ Y9) `
by A1, Lm1;
then
S c= (X9 `) \/ (Y9 `)
by XBOOLE_1:54;
then
S = ((X9 `) \/ (Y9 `)) /\ S
by XBOOLE_1:28;
then A4:
S = ((X9 `) /\ S) \/ ((Y9 `) /\ S)
by XBOOLE_1:23;
A5:
S is closed
by YELLOW_8:def 3;
Y9 is open
by A2, PRE_TOPC:def 2;
then
Y9 ` is closed
;
then A6:
(Y9 `) /\ S is closed
by A5;
X9 is open
by A2, PRE_TOPC:def 2;
then
X9 ` is closed
;
then
(X9 `) /\ S is closed
by A5;
then
( S = (X9 `) /\ S or S = (Y9 `) /\ S )
by A6, A4, YELLOW_8:def 3;
then
( S c= X9 ` or S c= Y9 ` )
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; verum