let L be sup-Semilattice; :: thesis: the carrier of (CompactSublatt L) is join-closed Subset of L
reconsider C = the carrier of (CompactSublatt L) as Subset of L 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 L by Def2; :: thesis: verum