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:43
.= x /\ (union D) by Th3
.= union { (x /\ d) where d is Element of D : verum } by Th1
.= sup ({x} "/\" D) by Th4 ; :: thesis: verum