let A be non empty RelStr ; :: thesis: for a being Element of A holds
( a is_<=_than the carrier of A iff for x being Element of A holds a <= x )
let a be Element of A; :: thesis: ( a is_<=_than the carrier of A iff for x being Element of A holds a <= x )
( ( for x being Element of A holds a <= x ) implies a is_<=_than the carrier of A )

proof

assume A1: for x being Element of A holds a <= x ; :: thesis: a is_<=_than the carrier of A
a is_<=_than the carrier of A

proof

let x be Element of A; :: according to LATTICE3:def 8 :: thesis: ( not x in the carrier of A or a <= x )
thus ( not x in the carrier of A or a <= x ) by A1; :: thesis: verum

end;

hence a is_<=_than the carrier of A ; :: thesis: verum

end;

hence ( a is_<=_than the carrier of A iff for x being Element of A holds a <= x ) by LATTICE3:def 8; :: thesis: verum