let L be complete LATTICE; :: thesis: for AR being Relation of L st ( 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 ) holds
AR is satisfying_SI
let AR be Relation of L; :: 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 ) implies AR is satisfying_SI )
assume A1: 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 ; :: thesis: AR is satisfying_SI

now :: thesis: for z, x being Element of L st [z,x] in AR & z <> x holds
ex y being Element of L st
( [z,y] in AR & [y,x] in AR & z <> y )

let z, x be Element of L; :: thesis: ( [z,x] in AR & z <> x implies ex y being Element of L st
( [y,b₃] in AR & [b₃,b₂] in AR & y <> b₃ ) )
assume that
A2: [z,x] in AR and
A3: z <> x ; :: thesis: ex y being Element of L st
( [y,b₃] in AR & [b₃,b₂] in AR & y <> b₃ )
A4: z in AR -below x by A2;

per cases ( [x,x] in AR or not [x,x] in AR ) ;

suppose [x,x] in AR ; :: thesis: ex y being Element of L st
( [y,b₃] in AR & [b₃,b₂] in AR & y <> b₃ )

hence ex y being Element of L st
( [z,y] in AR & [y,x] in AR & z <> y ) by A2, A3; :: thesis: verum

end;

suppose not [x,x] in AR ; :: thesis: ex y being Element of L st
( [y,b₃] in AR & [b₃,b₂] in AR & y <> b₃ )

then not z is_maximal_wrt AR -below x,AR by A1;
then consider y being set such that
A5: y in AR -below x and
A6: y <> z and
A7: [z,y] in AR by A4;
[y,x] in AR by A5, Th13;
hence ex y being Element of L st
( [z,y] in AR & [y,x] in AR & z <> y ) by A5, A6, A7; :: thesis: verum

end;

end;

end;

hence AR is satisfying_SI ; :: thesis: verum