let L be sup-Semilattice; :: thesis: the carrier of (CompactSublatt L) is join-closed Subset of
reconsider C = the carrier of (CompactSublatt L) as Subset of by YELLOW_0:def 13;
subrelstr C = CompactSublatt L by YELLOW_0:def 15;
hence the carrier of (CompactSublatt L) is join-closed Subset of by Def2; :: thesis: verum