let L be non empty up-complete Poset; :: thesis: ( L is finite implies the carrier of L = the carrier of (CompactSublatt L) )
assume A1: L is finite ; :: thesis: the carrier of L = the carrier of (CompactSublatt L)
A2: the carrier of L c= the carrier of (CompactSublatt L)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in the carrier of L or z in the carrier of (CompactSublatt L) )
assume z in the carrier of L ; :: thesis: z in the carrier of (CompactSublatt L)
then reconsider z1 = z as Element of L ;
z1 is compact by A1, WAYBEL_3:17;
hence z in the carrier of (CompactSublatt L) by WAYBEL_8:def 1; :: thesis: verum
end;
the carrier of (CompactSublatt L) c= the carrier of L by YELLOW_0:def 13;
hence the carrier of L = the carrier of (CompactSublatt L) by A2; :: thesis: verum