let L be complete Lattice; for a being Element of L st a is completely-join-irreducible holds
a % is join-irreducible
let a be Element of L; ( a is completely-join-irreducible implies a % is join-irreducible )
set X = { d where d is Element of L : ( d [= a & d <> a ) } ;
assume
a is completely-join-irreducible
; a % is join-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:
{ d where d is Element of L : ( d [= a & d <> a ) } is_less_than *' a
by LATTICE3:def 21;
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
x <= a %
by YELLOW_0:22;
then A9:
% x [= a
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
;
y <= a %
by A8, YELLOW_0:22;
then A13:
% y [= a
by A12, LATTICE3:7;
y = % y
by LATTICE3:def 4;
then
% y in { d where d is Element of L : ( d [= a & d <> a ) }
by A6, A13, A3, A11;
then
% y [= *' a
by A5, LATTICE3:def 17;
then A14:
(*' a) % >= y
by A12, LATTICE3:7;
x = % x
by LATTICE3:def 4;
then
% x in { d where d is Element of L : ( d [= a & d <> a ) }
by A6, A9, A3, A10;
then
% x [= *' a
by A5, LATTICE3:def 17;
then
(*' a) % >= x
by A7, LATTICE3:7;
then
(*' a) % >= a %
by A8, A14, YELLOW_0:22;
hence
contradiction
by A1, A2, A4, ORDERS_2:2;
verum
end;
hence
a % is join-irreducible
by WAYBEL_6:def 3; verum