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 meet-irreducible
let p be Element of L; :: thesis: for F being Filter of L st p is_maximal_in F ` holds
p is meet-irreducible
let F be Filter of L; :: thesis: ( p is_maximal_in F ` implies p is meet-irreducible )
assume A1: p is_maximal_in F ` ; :: thesis: p is meet-irreducible
set X = the carrier of L \ F;
A2: p in the carrier of L \ F by A1, WAYBEL_4:56;

now

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

now

assume ( x in F & y in F ) ; :: thesis: contradiction
then consider z being Element of L such that
A4: ( z in F & z <= x & z <= y ) by WAYBEL_0:def 2;
p >= z by A3, A4, YELLOW_0:23;
then p in F by A4, WAYBEL_0:def 20;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;

then A5: ( x in the carrier of L \ F or y in the carrier of L \ F ) by XBOOLE_0:def 5;
( p <= x & p <= y ) by A3, YELLOW_0:23;
then ( p < x & p < y ) by A3, ORDERS_2:def 10;
hence contradiction by A1, A5, WAYBEL_4:56; :: thesis: verum

end;

hence p is meet-irreducible by Def2; :: thesis: verum