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,b3] in AR & [b3,b2] in AR & y <> b3 ) )
assume that
A2: [z,x] in AR and
A3: z <> x ; :: thesis: ex y being Element of L st
( [y,b3] in AR & [b3,b2] in AR & y <> b3 )
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,b3] in AR & [b3,b2] in AR & y <> b3 )
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,b3] in AR & [b3,b2] in AR & y <> b3 )
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