let L be complete LATTICE; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: [x,x] in AR
A3: ( y in AR -below x & ( for y' being Element of L holds
( not y' in AR -below x or not y <> y' or not [y,y'] in AR ) ) ) by A2, Def24;
assume A4: not [x,x] in AR ; :: thesis: contradiction
A5: [y,x] in AR by A3, Th13;

per cases ( x = y or x <> y ) ;

suppose x = y ; :: thesis: contradiction

hence contradiction by A3, A4, Th13; :: thesis: verum

end;

suppose x <> y ; :: thesis: contradiction

then consider z being Element of L such that
A6: ( [y,z] in AR & [z,x] in AR & z <> y ) by A1, A5, Def21;
z in AR -below x by A6;
hence contradiction by A2, A6, Def24; :: thesis: verum

end;

end;