let X be set ; :: thesis: BoolePoset X is arithmetic

hence BoolePoset X is arithmetic by WAYBEL_8:19; :: thesis: verum

now :: thesis: for x, y being Element of (CompactSublatt (BoolePoset X)) holds ex_inf_of {x,y}, CompactSublatt (BoolePoset X)

then
CompactSublatt (BoolePoset X) is with_infima
by YELLOW_0:21;let x, y be Element of (CompactSublatt (BoolePoset X)); :: thesis: ex_inf_of {x,y}, CompactSublatt (BoolePoset X)

reconsider x9 = x, y9 = y as Element of (BoolePoset X) by YELLOW_0:58;

x9 is compact by WAYBEL_8:def 1;

then x9 is finite by WAYBEL_8:28;

then x9 /\ y9 is finite ;

then x9 "/\" y9 is finite by YELLOW_1:17;

then x9 "/\" y9 is compact by WAYBEL_8:28;

then reconsider xy = x9 "/\" y9 as Element of (CompactSublatt (BoolePoset X)) by WAYBEL_8:def 1;

then x9 "/\" y9 c= y9 by YELLOW_1:17;

then x9 "/\" y9 <= y9 by YELLOW_1:2;

then A5: xy <= y by YELLOW_0:60;

x9 /\ y9 c= x9 by XBOOLE_1:17;

then x9 "/\" y9 c= x9 by YELLOW_1:17;

then x9 "/\" y9 <= x9 by YELLOW_1:2;

then xy <= x by YELLOW_0:60;

hence ex_inf_of {x,y}, CompactSublatt (BoolePoset X) by A5, A1, YELLOW_0:19; :: thesis: verum

end;reconsider x9 = x, y9 = y as Element of (BoolePoset X) by YELLOW_0:58;

x9 is compact by WAYBEL_8:def 1;

then x9 is finite by WAYBEL_8:28;

then x9 /\ y9 is finite ;

then x9 "/\" y9 is finite by YELLOW_1:17;

then x9 "/\" y9 is compact by WAYBEL_8:28;

then reconsider xy = x9 "/\" y9 as Element of (CompactSublatt (BoolePoset X)) by WAYBEL_8:def 1;

A1: now :: thesis: for z being Element of (CompactSublatt (BoolePoset X)) st z <= x & z <= y holds

xy >= z

x9 /\ y9 c= y9
by XBOOLE_1:17;xy >= z

let z be Element of (CompactSublatt (BoolePoset X)); :: thesis: ( z <= x & z <= y implies xy >= z )

reconsider z9 = z as Element of (BoolePoset X) by YELLOW_0:58;

assume that

A2: z <= x and

A3: z <= y ; :: thesis: xy >= z

z9 <= y9 by A3, YELLOW_0:59;

then A4: z9 c= y9 by YELLOW_1:2;

z9 <= x9 by A2, YELLOW_0:59;

then z9 c= x9 by YELLOW_1:2;

then z9 c= x9 /\ y9 by A4, XBOOLE_1:19;

then z9 c= x9 "/\" y9 by YELLOW_1:17;

then z9 <= x9 "/\" y9 by YELLOW_1:2;

hence xy >= z by YELLOW_0:60; :: thesis: verum

end;reconsider z9 = z as Element of (BoolePoset X) by YELLOW_0:58;

assume that

A2: z <= x and

A3: z <= y ; :: thesis: xy >= z

z9 <= y9 by A3, YELLOW_0:59;

then A4: z9 c= y9 by YELLOW_1:2;

z9 <= x9 by A2, YELLOW_0:59;

then z9 c= x9 by YELLOW_1:2;

then z9 c= x9 /\ y9 by A4, XBOOLE_1:19;

then z9 c= x9 "/\" y9 by YELLOW_1:17;

then z9 <= x9 "/\" y9 by YELLOW_1:2;

hence xy >= z by YELLOW_0:60; :: thesis: verum

then x9 "/\" y9 c= y9 by YELLOW_1:17;

then x9 "/\" y9 <= y9 by YELLOW_1:2;

then A5: xy <= y by YELLOW_0:60;

x9 /\ y9 c= x9 by XBOOLE_1:17;

then x9 "/\" y9 c= x9 by YELLOW_1:17;

then x9 "/\" y9 <= x9 by YELLOW_1:2;

then xy <= x by YELLOW_0:60;

hence ex_inf_of {x,y}, CompactSublatt (BoolePoset X) by A5, A1, YELLOW_0:19; :: thesis: verum

hence BoolePoset X is arithmetic by WAYBEL_8:19; :: thesis: verum