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

now :: thesis: for x, y being Element of (CompactSublatt (InclPoset (Ids S))) 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 ) )

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:58;
x1 is compact by WAYBEL_8:def 1;
then consider a being Element of S such that
A1: x1 = downarrow a by Th12;
y1 is compact by WAYBEL_8:def 1;
then consider b being Element of S such that
A2: y1 = downarrow b by Th12;
Bottom S <= b by YELLOW_0:44;
then A3: Bottom S in downarrow b by WAYBEL_0:17;
Bottom S <= a by YELLOW_0:44;
then Bottom S in downarrow a by WAYBEL_0:17;
then reconsider xy = (downarrow a) /\ (downarrow b) as non empty Subset of S by A3, 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 A1, A2, YELLOW_1:9;
then reconsider z1 = (downarrow a) /\ (downarrow b) as Element of (InclPoset (Ids S)) ;
z1 c= y1 by A2, XBOOLE_1:17;
then A4: z1 <= y1 by YELLOW_1:3;
A5: downarrow (a "/\" b) c= (downarrow a) /\ (downarrow b)

proof

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

end;

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

proof

let v be object ; :: according to TARSKI:def 3 :: thesis: ( not v in (downarrow a) /\ (downarrow b) or v in downarrow (a "/\" b) )
assume A9: v in (downarrow a) /\ (downarrow b) ; :: thesis: v in downarrow (a "/\" b)
then reconsider v1 = v as Element of S ;
v in downarrow b by A9, XBOOLE_0:def 4;
then A10: v1 <= b by WAYBEL_0:17;
v in downarrow a by A9, XBOOLE_0:def 4;
then v1 <= a by WAYBEL_0:17;
then v1 <= a "/\" b by A10, YELLOW_0:23;
hence v in downarrow (a "/\" b) by WAYBEL_0:17; :: 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 by A1, XBOOLE_1:17;
then z1 <= x1 by YELLOW_1:3;
hence ( z <= x & z <= y ) by A4, YELLOW_0:60; :: 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:58;
assume that
A11: v <= x and
A12: v <= y ; :: thesis: v <= z
v1 <= y1 by A12, YELLOW_0:59;
then A13: v1 c= y1 by YELLOW_1:3;
v1 <= x1 by A11, YELLOW_0:59;
then v1 c= x1 by YELLOW_1:3;
then v1 c= z1 by A1, A2, A13, XBOOLE_1:19;
then v1 <= z1 by YELLOW_1:3;
hence v <= z by YELLOW_0:60; :: thesis: verum

end;

then A14: CompactSublatt (InclPoset (Ids S)) is with_infima by LATTICE3:def 11;
InclPoset (Ids S) is algebraic by Th10;
hence InclPoset (Ids S) is arithmetic by A14, WAYBEL_8:19; :: thesis: verum