let L be non empty RelStr ; :: thesis: for p being Element of L st p is completely-irreducible holds
"/\" (((uparrow p) \ {p}),L) <> p
let p be Element of L; :: thesis: ( p is completely-irreducible implies "/\" (((uparrow p) \ {p}),L) <> p )
assume p is completely-irreducible ; :: thesis: "/\" (((uparrow p) \ {p}),L) <> p
then ex_min_of (uparrow p) \ {p},L ;
then "/\" (((uparrow p) \ {p}),L) in (uparrow p) \ {p} by WAYBEL_1:def 4;
then not "/\" (((uparrow p) \ {p}),L) in {p} by XBOOLE_0:def 5;
hence "/\" (((uparrow p) \ {p}),L) <> p by TARSKI:def 1; :: thesis: verum