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 ( not x << x & x << y ) ; :: according to WAYBEL_3:def 2 :: thesis: x < y
hence ( x <= y & x <> y ) by Th1; :: according to ORDERS_2:def 10 :: thesis: verum