set I = InclPoset (Ids R);
let x be Element of (InclPoset (Ids R)); :: according to WAYBEL_2:def 6 :: thesis: for b₁ being Element of bool the carrier of (InclPoset (Ids R)) holds x "/\" ("\/" b₁,(InclPoset (Ids R))) = "\/" ({x} "/\" b₁),(InclPoset (Ids R))
let D be non empty directed Subset of (InclPoset (Ids R)); :: thesis: x "/\" ("\/" D,(InclPoset (Ids R))) = "\/" ({x} "/\" D),(InclPoset (Ids R))
thus x "/\" (sup D) = x /\ (sup D) by YELLOW_2:45
.= x /\ (union D) by Th3
.= union { (x /\ d) where d is Element of D : verum } by Th1
.= sup ({x} "/\" D) by Th4 ; :: thesis: verum