let L be complete LATTICE; :: thesis: for x, y, k being Element of L st x <= k & k <= y & k in the carrier of (CompactSublatt L) holds
x << y
let x, y, k be Element of L; :: thesis: ( x <= k & k <= y & k in the carrier of (CompactSublatt L) implies x << y )
assume that
A1: ( x <= k & k <= y ) and
A2: k in the carrier of (CompactSublatt L) ; :: thesis: x << y
k is compact by A2, Def1;
then k << k by WAYBEL_3:def 2;
hence x << y by A1, WAYBEL_3:2; :: thesis: verum