theorem Th13: :: WAYBEL20:13

for L being non empty antisymmetric RelStr
for X being Subset of [:L,L:] st X c= id the carrier of L & ex_inf_of X,[:L,L:] holds
inf X in id the carrier of L