theorem Th62: :: WAYBEL_1:62

for S being Semilattice holds
( ( for x being Element of S holds x "/\" is lower_adjoint ) iff for x, t being Element of S holds ex_max_of { s where s is Element of S : x "/\" s <= t } ,S )