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