let L be Semilattice; Irr L c= IRR L
let x be object ; TARSKI:def 3 ( not x in Irr L or x in IRR L )
assume A1:
x in Irr L
; x in IRR L
then reconsider x1 = x as Element of L ;
x1 is completely-irreducible
by A1, Def4;
then consider q being Element of L such that
A2:
x1 < q
and
A3:
for s being Element of L st x1 < s holds
q <= s
and
uparrow x1 = {x1} \/ (uparrow q)
by Th20;
now for a, b being Element of L st x1 = a "/\" b & a <> x1 holds
not b <> x1let a,
b be
Element of
L;
( x1 = a "/\" b & a <> x1 implies not b <> x1 )assume that A4:
x1 = a "/\" b
and A5:
a <> x1
and A6:
b <> x1
;
contradiction
x1 <= b
by A4, YELLOW_0:23;
then
x1 < b
by A6, ORDERS_2:def 6;
then A7:
q <= b
by A3;
A8:
x1 <= q
by A2, ORDERS_2:def 6;
x1 <= a
by A4, YELLOW_0:23;
then
x1 < a
by A5, ORDERS_2:def 6;
then
q <= a
by A3;
then
q <= x1
by A4, A7, YELLOW_0:23;
hence
contradiction
by A2, A8, ORDERS_2:2;
verum end;
then
x1 is irreducible
by WAYBEL_6:def 2;
hence
x in IRR L
by WAYBEL_6:def 4; verum