let L be lower-bounded algebraic LATTICE; :: thesis: for s being Element of L holds s = "/\" (((uparrow s) /\ (Irr L)),L)
let s be Element of L; :: thesis: s = "/\" (((uparrow s) /\ (Irr L)),L)
Irr L is order-generating by Th32;
hence s = "/\" (((uparrow s) /\ (Irr L)),L) by WAYBEL_6:def 5; :: thesis: verum