theorem :: YELLOW_4:40

for L being reflexive antisymmetric with_infima RelStr
for A being Subset of L holds A c= A "/\" A