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 object 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 object 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;

then U_FT z2 meets A by A3, A5, XBOOLE_0:3;

then A9: z in A ^b ;

(A ^b) /\ B = {} by A2;

hence contradiction by A8, A9, XBOOLE_0:def 4; :: thesis: verum

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 object 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 object 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;

then U_FT z2 meets A by A3, A5, XBOOLE_0:3;

then A9: z in A ^b ;

(A ^b) /\ B = {} by A2;

hence contradiction by A8, A9, XBOOLE_0:def 4; :: thesis: verum