let FT be non empty 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 A1: ( FT is symmetric & A ^b misses B ) ; :: thesis: A misses B ^b
then A2: (A ^b ) /\ B = {} by XBOOLE_0:def 7;
assume A meets B ^b ; :: thesis: contradiction
then consider x being set such that
A3: ( x in A & x in B ^b ) by XBOOLE_0:3;
consider y being Element of FT such that
A4: ( x = y & U_FT y meets B ) by A3;
consider z being set such that
A5: ( z in U_FT y & z in B ) by A4, XBOOLE_0:3;
reconsider z2 = z as Element of FT by A5;
y in U_FT z2 by A1, A5, FIN_TOPO:def 15;
then U_FT z2 meets A by A3, A4, XBOOLE_0:3;
then z in A ^b ;
hence contradiction by A2, A5, XBOOLE_0:def 4; :: thesis: verum