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 by Def3;
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