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