theorem :: WAYBEL16:33

for L being lower-bounded algebraic LATTICE
for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L)