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

proof

assume A misses B ; :: thesis: B c= A `
then A /\ B = {} T by XBOOLE_0:def 7;
then (A /\ B) ` = [#] T ;
then (B ` ) \/ (A ` ) = [#] T by XBOOLE_1:54;
then (B ` ) ` c= A ` by Th1;
hence B c= A ` ; :: thesis: verum

end;

assume B c= A ` ; :: thesis: A misses B
then (B ` ) ` c= A ` ;
then (B ` ) \/ (A ` ) = [#] T by Th1;
then (A /\ B) ` = [#] T by XBOOLE_1:54;
then A /\ B = ([#] T) ` ;
then A /\ B = {} T by XBOOLE_1:37;
hence A misses B by XBOOLE_0:def 7; :: thesis: verum