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 ` )
A1: A in bool E by Def2;
assume that
A2: A misses B and
A3: A ` misses B ` ; :: thesis: A = B `
thus A c= B ` :: according to XBOOLE_0:def 10 :: thesis: B ` c= A

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B ` )
assume A4: x in A ; :: thesis: x in B `
A c= E by A1, ZFMISC_1:def 1;
then A5: x in E by A4, TARSKI:def 3;
not x in B by A2, A4, XBOOLE_0:3;
hence x in B ` by A5, XBOOLE_0:def 5; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in B ` or x in A )
assume x in B ` ; :: thesis: x in A
then A6: ( x in E & not x in B ) by XBOOLE_0:def 5;
( x in A ` implies not x in B ` ) by A3, XBOOLE_0:3;
hence x in A by A6, XBOOLE_0:def 5; :: thesis: verum