let L be non empty with_suprema lower-bounded Poset; :: thesis: ( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )

now

let x, y be Element of L; :: thesis: ( x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_sup_of {x,y},L implies sup {x,y} in the carrier of (CompactSublatt L) )
assume that
A1: x in the carrier of (CompactSublatt L) and
A2: y in the carrier of (CompactSublatt L) and
A3: ex_sup_of {x,y},L ; :: thesis: sup {x,y} in the carrier of (CompactSublatt L)
y is compact by A2, Def1;
then A4: y << y by WAYBEL_3:def 2;
x is compact by A1, Def1;
then A5: x << x by WAYBEL_3:def 2;
y <= x "\/" y by A3, YELLOW_0:18;
then A6: y << x "\/" y by A4, WAYBEL_3:2;
x <= x "\/" y by A3, YELLOW_0:18;
then x << x "\/" y by A5, WAYBEL_3:2;
then x "\/" y << x "\/" y by A6, WAYBEL_3:3;
then x "\/" y is compact by WAYBEL_3:def 2;
then sup {x,y} is compact by YELLOW_0:41;
hence sup {x,y} in the carrier of (CompactSublatt L) by Def1; :: thesis: verum

end;

hence CompactSublatt L is join-inheriting by YELLOW_0:def 17; :: thesis: Bottom L in the carrier of (CompactSublatt L)
Bottom L is compact by WAYBEL_3:15;
hence Bottom L in the carrier of (CompactSublatt L) by Def1; :: thesis: verum