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

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