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

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