theorem Th42: :: YELLOW_3:42

for S1, S2 being non empty antisymmetric RelStr
for D being Subset of [:S1,S2:] holds
( ( ex_inf_of proj1 D,S1 & ex_inf_of proj2 D,S2 ) iff ex_inf_of D,[:S1,S2:] )