let E be set ; :: thesis: for A, B being Subset of E holds
( A misses B iff A c= B ` )
let A, B be Subset of E; :: thesis: ( A misses B iff A c= B ` )
thus ( A misses B implies A c= B ` ) :: thesis: ( A c= B ` implies A misses B )

proof

assume A1: A misses B ; :: thesis: A c= B `
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B ` )
assume A2: x in A ; :: thesis: x in B `
then A3: not x in B by A1, XBOOLE_0:3;
x in E by A2, Lm1;
hence x in B ` by A3, XBOOLE_0:def 5; :: thesis: verum

end;

assume A4: A c= B ` ; :: thesis: A misses B
assume A meets B ; :: thesis: contradiction
then consider x being object such that
A5: x in A and
A6: x in B by XBOOLE_0:3;
x in E \ B by A4, A5;
hence contradiction by A6, XBOOLE_0:def 5; :: thesis: verum