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

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 A2: ( [z,x] in AR & z <> x ) ; :: thesis: ex y being Element of L st
( [y,b₃] in AR & [b₃,b₂] in AR & y <> b₃ )
then A3: z in AR -below x ;

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; :: 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
A4: ( y in AR -below x & y <> z & [z,y] in AR ) by A3, Def24;
[y,x] in AR by A4, Th13;
hence ex y being Element of L st
( [z,y] in AR & [y,x] in AR & z <> y ) by A4; :: thesis: verum

end;

end;

end;

hence AR is satisfying_SI by Def21; :: thesis: verum