theorem Th25: :: WAYBEL12:25

for L being transitive antisymmetric with_infima RelStr
for V being upper Subset of L holds { x where x is Element of L : V "/\" {x} c= V } is upper Subset of L