let L be complete Lattice; for a being Element of L st a is completely-meet-irreducible holds
a % is meet-irreducible
let a be Element of L; ( a is completely-meet-irreducible implies a % is meet-irreducible )
set X = { d where d is Element of L : ( a [= d & d <> a ) } ;
assume
a is completely-meet-irreducible
; a % is meet-irreducible
then A1:
a <> a *'
;
for x, y being Element of (LattPOSet L) holds
( not a % = x "/\" y or x = a % or y = a % )
proof
a [= a *'
by Th9;
then A2:
a % <= (a *') %
by LATTICE3:7;
A3:
% (a %) = a %
by LATTICE3:def 4;
A4:
(
a = a % &
a *' = (a *') % )
by LATTICE3:def 3;
A5:
a *' is_less_than { d where d is Element of L : ( a [= d & d <> a ) }
by LATTICE3:34;
let x,
y be
Element of
(LattPOSet L);
( not a % = x "/\" y or x = a % or y = a % )
A6:
a =
a %
by LATTICE3:def 3
.=
% (a %)
by LATTICE3:def 4
;
A7:
x =
% x
by LATTICE3:def 4
.=
(% x) %
by LATTICE3:def 3
;
assume A8:
a % = x "/\" y
;
( x = a % or y = a % )
then
a % <= x
by YELLOW_0:23;
then A9:
a [= % x
by A7, LATTICE3:7;
assume that A10:
x <> a %
and A11:
y <> a %
;
contradiction
A12:
y =
% y
by LATTICE3:def 4
.=
(% y) %
by LATTICE3:def 3
;
a % <= y
by A8, YELLOW_0:23;
then A13:
a [= % y
by A12, LATTICE3:7;
y = % y
by LATTICE3:def 4;
then
% y in { d where d is Element of L : ( a [= d & d <> a ) }
by A6, A13, A3, A11;
then
a *' [= % y
by A5, LATTICE3:def 16;
then A14:
(a *') % <= (% y) %
by LATTICE3:7;
x = % x
by LATTICE3:def 4;
then
% x in { d where d is Element of L : ( a [= d & d <> a ) }
by A6, A9, A3, A10;
then
a *' [= % x
by A5, LATTICE3:def 16;
then
(a *') % <= (% x) %
by LATTICE3:7;
then
(a *') % <= a %
by A8, A12, A7, A14, YELLOW_0:23;
hence
contradiction
by A1, A2, A4, ORDERS_2:2;
verum
end;
hence
a % is meet-irreducible
by WAYBEL_6:def 2; verum