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 by A2;
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 and
A7: [z,x] in AR and
A8: z <> y by A1, A5;
z in AR -below x by A7;
hence contradiction by A2, A6, A8; :: thesis: verum
end;
end;