let L be complete LATTICE; for AR being Relation of L st AR is satisfying_SI holds
for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR
let AR be Relation of L; ( AR is satisfying_SI implies for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR )
assume A1:
AR is satisfying_SI
; for x being Element of L st ex y being Element of L st y is_maximal_wrt AR -below x,AR holds
[x,x] in AR
let x be Element of L; ( ex y being Element of L st y is_maximal_wrt AR -below x,AR implies [x,x] in AR )
given y being Element of L such that A2:
y is_maximal_wrt AR -below x,AR
; [x,x] in AR
A3:
y in AR -below x
by A2;
assume A4:
not [x,x] in AR
; contradiction
A5:
[y,x] in AR
by A3, Th13;