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