set I = InclPoset (Ids R);

let x be Element of (InclPoset (Ids R)); :: according to WAYBEL_2:def 6 :: thesis: for b_{1} being Element of bool the carrier of (InclPoset (Ids R)) holds x "/\" ("\/" (b_{1},(InclPoset (Ids R)))) = "\/" (({x} "/\" b_{1}),(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

let x be Element of (InclPoset (Ids R)); :: according to WAYBEL_2:def 6 :: thesis: for b

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