let L be non empty with_suprema lower-bounded Poset; ( CompactSublatt L is join-inheriting & Bottom L in the carrier of (CompactSublatt L) )
now for x, y being Element of L st x in the carrier of (CompactSublatt L) & y in the carrier of (CompactSublatt L) & ex_sup_of {x,y},L holds
sup {x,y} in the carrier of (CompactSublatt L)let x,
y be
Element of
L;
( 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
;
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;
verum end;
hence
CompactSublatt L is join-inheriting
by YELLOW_0:def 17; 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; verum