theorem Th14: :: FIN_TOPO:14

for FT being non empty RelStr
for A, B being Subset of FT st A c= B holds
A ^b c= B ^b