theorem Th26: :: YELLOW_2:26

for L being non empty RelStr st ( for A being Subset of L holds ex_inf_of A,L ) holds
for X being set holds
( ex_inf_of X,L & "/\" (X,L) = "/\" ((X /\ the carrier of L),L) )