let S be lower-bounded LATTICE; :: thesis: InclPoset (Ids S) is arithmetic
A1: InclPoset (Ids S) is algebraic by Th10;

now

let x, y be Element of (CompactSublatt (InclPoset (Ids S))); :: thesis: ex z being Element of (CompactSublatt (InclPoset (Ids S))) st
( z <= x & z <= y & ( for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds
v <= z ) )
reconsider x1 = x, y1 = y as Element of (InclPoset (Ids S)) by YELLOW_0:59;
A2: ( x1 is compact & y1 is compact ) by WAYBEL_8:def 1;
then consider a being Element of S such that
A3: x1 = downarrow a by Th12;
consider b being Element of S such that
A4: y1 = downarrow b by A2, Th12;
( Bottom S <= a & Bottom S <= b ) by YELLOW_0:44;
then ( Bottom S in downarrow a & Bottom S in downarrow b ) by WAYBEL_0:17;
then reconsider xy = (downarrow a) /\ (downarrow b) as non empty Subset of S by XBOOLE_0:def 4;
reconsider xy = xy as non empty lower Subset of S by WAYBEL_0:27;
reconsider xy = xy as non empty directed lower Subset of S by WAYBEL_0:44;
xy is Ideal of S ;
then (downarrow a) /\ (downarrow b) in { X where X is Ideal of S : verum } ;
then (downarrow a) /\ (downarrow b) in Ids S by WAYBEL_0:def 23;
then x1 "/\" y1 = (downarrow a) /\ (downarrow b) by A3, A4, YELLOW_1:9;
then reconsider z1 = (downarrow a) /\ (downarrow b) as Element of (InclPoset (Ids S)) ;
A5: (downarrow a) /\ (downarrow b) c= downarrow (a "/\" b)

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in (downarrow a) /\ (downarrow b) or v in downarrow (a "/\" b) )
assume A6: v in (downarrow a) /\ (downarrow b) ; :: thesis: v in downarrow (a "/\" b)
then A7: ( v in downarrow a & v in downarrow b ) by XBOOLE_0:def 4;
reconsider v1 = v as Element of S by A6;
( v1 <= a & v1 <= b ) by A7, WAYBEL_0:17;
then v1 <= a "/\" b by YELLOW_0:23;
hence v in downarrow (a "/\" b) by WAYBEL_0:17; :: thesis: verum

end;

downarrow (a "/\" b) c= (downarrow a) /\ (downarrow b)

proof

let v be set ; :: according to TARSKI:def 3 :: thesis: ( not v in downarrow (a "/\" b) or v in (downarrow a) /\ (downarrow b) )
assume A8: v in downarrow (a "/\" b) ; :: thesis: v in (downarrow a) /\ (downarrow b)
then reconsider v1 = v as Element of S ;
A9: v1 <= a "/\" b by A8, WAYBEL_0:17;
( a "/\" b <= a & a "/\" b <= b ) by YELLOW_0:23;
then ( v1 <= a & v1 <= b ) by A9, ORDERS_2:26;
then ( v in downarrow a & v in downarrow b ) by WAYBEL_0:17;
hence v in (downarrow a) /\ (downarrow b) by XBOOLE_0:def 4; :: thesis: verum

end;

then z1 = downarrow (a "/\" b) by A5, XBOOLE_0:def 10;
then z1 is compact by Th12;
then reconsider z = z1 as Element of (CompactSublatt (InclPoset (Ids S))) by WAYBEL_8:def 1;
take z = z; :: thesis: ( z <= x & z <= y & ( for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds
v <= z ) )
( z1 c= x1 & z1 c= y1 ) by A3, A4, XBOOLE_1:17;
then ( z1 <= x1 & z1 <= y1 ) by YELLOW_1:3;
hence ( z <= x & z <= y ) by YELLOW_0:61; :: thesis: for v being Element of (CompactSublatt (InclPoset (Ids S))) st v <= x & v <= y holds
v <= z
let v be Element of (CompactSublatt (InclPoset (Ids S))); :: thesis: ( v <= x & v <= y implies v <= z )
reconsider v1 = v as Element of (InclPoset (Ids S)) by YELLOW_0:59;
assume ( v <= x & v <= y ) ; :: thesis: v <= z
then ( v1 <= x1 & v1 <= y1 ) by YELLOW_0:60;
then ( v1 c= x1 & v1 c= y1 ) by YELLOW_1:3;
then v1 c= z1 by A3, A4, XBOOLE_1:19;
then v1 <= z1 by YELLOW_1:3;
hence v <= z by YELLOW_0:61; :: thesis: verum

end;

then CompactSublatt (InclPoset (Ids S)) is with_infima by LATTICE3:def 11;
hence InclPoset (Ids S) is arithmetic by A1, WAYBEL_8:21; :: thesis: verum