Bottom L in the carrier of (CompactSublatt L) by WAYBEL_8:3;
then CompactSublatt L is non empty full join-inheriting bottom-inheriting SubRelStr of L by Def19;
hence CompactSublatt L is finite-sups-inheriting ; :: thesis: verum