let L be non empty reflexive antisymmetric RelStr ; :: thesis: for x, y being Element of L st not x is compact & x << y holds
x < y
let x, y be Element of L; :: thesis: ( not x is compact & x << y implies x < y )
assume that
A1: not x << x and
A2: x << y ; :: according to WAYBEL_3:def 2 :: thesis: x < y
thus ( x <= y & x <> y ) by A1, A2, Th1; :: according to ORDERS_2:def 6 :: thesis: verum