theorem thre1: :: FIELD_5:10

for X, Y being set st card X c= card Y holds
ex Z being set st
( Z c= Y & card Z = card X )