let E be set ; :: thesis: for A, B being Subset of E st A misses B & A ` misses B ` holds
A = B `
let A, B be Subset of E; :: thesis: ( A misses B & A ` misses B ` implies A = B ` )
assume that
A1: A misses B and
A2: A ` misses B ` ; :: thesis: A = B `
A3: A in bool E by Def1;
thus A c= B ` :: according to XBOOLE_0:def 10 :: thesis: B ` c= A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B ` )
assume A4: x in A ; :: thesis: x in B `
then A5: not x in B by A1, XBOOLE_0:3;
A c= E by A3, ZFMISC_1:def 1;
then x in E by A4;
hence x in B ` by A5, XBOOLE_0:def 5; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in B ` or x in A )
A6: ( x in A ` implies not x in B ` ) by A2, XBOOLE_0:3;
assume A7: x in B ` ; :: thesis: x in A
then x in E by XBOOLE_0:def 5;
hence x in A by A7, A6, XBOOLE_0:def 5; :: thesis: verum