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)

hence the carrier of L = the carrier of (CompactSublatt L) by A2; :: thesis: verum

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

the carrier of (CompactSublatt L) c= the carrier of L
by YELLOW_0:def 13;
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;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

hence the carrier of L = the carrier of (CompactSublatt L) by A2; :: thesis: verum