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

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

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;

A1: now :: thesis: for z being Element of (CompactSublatt (BoolePoset X)) st z <= x & z <= y holds
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;

x9 /\ y9 c= y9 by XBOOLE_1:17;
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;

then CompactSublatt (BoolePoset X) is with_infima by YELLOW_0:21;
hence BoolePoset X is arithmetic by WAYBEL_8:19; :: thesis: verum