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