let FT be non empty filled RelStr ; :: thesis: for A, B being Subset of FT st FT is symmetric & A ^b misses B holds
A misses B ^b
let A, B be Subset of FT; :: thesis: ( FT is symmetric & A ^b misses B implies A misses B ^b )
assume that
A1: FT is symmetric and
A2: A ^b misses B ; :: thesis: A misses B ^b

now :: thesis: not A meets B ^b

assume A meets B ^b ; :: thesis: contradiction
then consider x being object such that
A3: x in A and
A4: x in B ^b by XBOOLE_0:3;
consider x2 being Element of FT such that
A5: x2 = x and
A6: U_FT x2 meets B by A4;
set y = the Element of (U_FT x2) /\ B;
A7: (U_FT x2) /\ B <> {} by A6, XBOOLE_0:def 7;
then A8: the Element of (U_FT x2) /\ B in U_FT x2 by XBOOLE_0:def 4;
then reconsider y2 = the Element of (U_FT x2) /\ B as Element of FT ;
x2 in U_FT y2 by A1, A8;
then x2 in (U_FT y2) /\ A by A3, A5, XBOOLE_0:def 4;
then U_FT y2 meets A by XBOOLE_0:def 7;
then A9: y2 in A ^b ;
the Element of (U_FT x2) /\ B in B by A7, XBOOLE_0:def 4;
hence contradiction by A2, A9, XBOOLE_0:3; :: thesis: verum

end;

hence A misses B ^b ; :: thesis: verum