let L be RelStr ; :: thesis: for a being Element of L holds
( {} is_<=_than a & {} is_>=_than a )
let a be Element of L; :: thesis: ( {} is_<=_than a & {} is_>=_than a )
thus {} is_<=_than a :: thesis: {} is_>=_than a

proof

let b be Element of L; :: according to LATTICE3:def 9 :: thesis: ( not b in {} or b <= a )
thus ( not b in {} or b <= a ) ; :: thesis: verum

end;

let b be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not b in {} or a <= b )
thus ( not b in {} or a <= b ) ; :: thesis: verum