let FT be non empty RelStr ; :: thesis: ({} FT) ^b = {}
assume not ({} FT) ^b = {} ; :: thesis: contradiction
then consider x being object such that
A1: x in ({} FT) ^b by XBOOLE_0:def 1;
ex y being Element of FT st
( x = y & U_FT y meets {} FT ) by A1;
hence contradiction ; :: thesis: verum