let L be non empty RelStr ; :: thesis: ( L is reflexive & L is connected implies ( L is with_infima & L is with_suprema ) )
assume A1: ( L is reflexive & L is connected ) ; :: thesis: ( L is with_infima & L is with_suprema )
thus L is with_infima :: thesis: L is with_suprema
proof
let x, y be Element of L; :: according to LATTICE3:def 11 :: thesis: ex b1 being Element of the carrier of L st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )

per cases ( x <= y or y <= x ) by A1;
suppose A2: x <= y ; :: thesis: ex b1 being Element of the carrier of L st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )

take z = x; :: thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )

thus ( z <= x & z <= y ) by A1, A2; :: thesis: for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z )

thus for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z ) ; :: thesis: verum
end;
suppose A3: y <= x ; :: thesis: ex b1 being Element of the carrier of L st
( b1 <= x & b1 <= y & ( for b2 being Element of the carrier of L holds
( not b2 <= x or not b2 <= y or b2 <= b1 ) ) )

take z = y; :: thesis: ( z <= x & z <= y & ( for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z ) ) )

thus ( z <= x & z <= y ) by A1, A3; :: thesis: for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z )

thus for b1 being Element of the carrier of L holds
( not b1 <= x or not b1 <= y or b1 <= z ) ; :: thesis: verum
end;
end;
end;
let x, y be Element of L; :: according to LATTICE3:def 10 :: thesis: ex b1 being Element of the carrier of L st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )

per cases ( x <= y or y <= x ) by A1;
suppose A4: x <= y ; :: thesis: ex b1 being Element of the carrier of L st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )

take z = y; :: thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )

thus ( z >= x & z >= y ) by A1, A4; :: thesis: for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 )

thus for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 ) ; :: thesis: verum
end;
suppose A5: y <= x ; :: thesis: ex b1 being Element of the carrier of L st
( x <= b1 & y <= b1 & ( for b2 being Element of the carrier of L holds
( not x <= b2 or not y <= b2 or b1 <= b2 ) ) )

take z = x; :: thesis: ( x <= z & y <= z & ( for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 ) ) )

thus ( z >= x & z >= y ) by A1, A5; :: thesis: for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 )

thus for b1 being Element of the carrier of L holds
( not x <= b1 or not y <= b1 or z <= b1 ) ; :: thesis: verum
end;
end;