CompactSublatt L is bottom-inheriting

proof

thus Bottom L in the carrier of (CompactSublatt L) by WAYBEL_8:3; :: according to WAYBEL34:def 19 :: thesis: verum

end;

then CompactSublatt L is non empty full join-inheriting bottom-inheriting SubRelStr of L ;
hence CompactSublatt L is finite-sups-inheriting ; :: thesis: verum