let L be LATTICE; :: thesis: for p being Element of L

for F being Filter of L st p is_maximal_in F ` holds

p is irreducible

let p be Element of L; :: thesis: for F being Filter of L st p is_maximal_in F ` holds

p is irreducible

let F be Filter of L; :: thesis: ( p is_maximal_in F ` implies p is irreducible )

assume A1: p is_maximal_in F ` ; :: thesis: p is irreducible

set X = the carrier of L \ F;

A2: p in the carrier of L \ F by A1, WAYBEL_4:55;

for F being Filter of L st p is_maximal_in F ` holds

p is irreducible

let p be Element of L; :: thesis: for F being Filter of L st p is_maximal_in F ` holds

p is irreducible

let F be Filter of L; :: thesis: ( p is_maximal_in F ` implies p is irreducible )

assume A1: p is_maximal_in F ` ; :: thesis: p is irreducible

set X = the carrier of L \ F;

A2: p in the carrier of L \ F by A1, WAYBEL_4:55;

now :: thesis: for x, y being Element of L st p = x "/\" y & x <> p holds

not y <> p

hence
p is irreducible
; :: thesis: verumnot y <> p

let x, y be Element of L; :: thesis: ( p = x "/\" y & x <> p implies not y <> p )

assume that

A3: p = x "/\" y and

A4: x <> p and

A5: y <> p ; :: thesis: contradiction

p <= y by A3, YELLOW_0:23;

then A6: p < y by A5, ORDERS_2:def 6;

p <= x by A3, YELLOW_0:23;

then p < x by A4, ORDERS_2:def 6;

hence contradiction by A1, A9, A6, WAYBEL_4:55; :: thesis: verum

end;assume that

A3: p = x "/\" y and

A4: x <> p and

A5: y <> p ; :: thesis: contradiction

p <= y by A3, YELLOW_0:23;

then A6: p < y by A5, ORDERS_2:def 6;

now :: thesis: ( x in F implies not y in F )

then A9:
( x in the carrier of L \ F or y in the carrier of L \ F )
by XBOOLE_0:def 5;assume
( x in F & y in F )
; :: thesis: contradiction

then consider z being Element of L such that

A7: z in F and

A8: ( z <= x & z <= y ) by WAYBEL_0:def 2;

p >= z by A3, A8, YELLOW_0:23;

then p in F by A7, WAYBEL_0:def 20;

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;then consider z being Element of L such that

A7: z in F and

A8: ( z <= x & z <= y ) by WAYBEL_0:def 2;

p >= z by A3, A8, YELLOW_0:23;

then p in F by A7, WAYBEL_0:def 20;

hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

p <= x by A3, YELLOW_0:23;

then p < x by A4, ORDERS_2:def 6;

hence contradiction by A1, A9, A6, WAYBEL_4:55; :: thesis: verum