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)
A4: ( x <= x "\/" y & y <= x "\/" y ) by A3, YELLOW_0:18;
x is compact by A1, Def1;
then x << x by WAYBEL_3:def 2;
then A5: x << x "\/" y by A4, WAYBEL_3:2;
y is compact by A2, Def1;
then y << y by WAYBEL_3:def 2;
then y << x "\/" y by A4, WAYBEL_3:2;
then x "\/" y << x "\/" y by A5, 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