the carrier of (CLatt L) = the carrier of L by Def11;
hence not CLatt L is empty ; :: thesis: verum