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;

now :: thesis: for x, y being Element of L st p = x "/\" y & x <> p holds
not 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;

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

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 A9: ( x in the carrier of L \ F or y in the carrier of L \ F ) by XBOOLE_0:def 5;
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;

hence p is irreducible ; :: thesis: verum