let T be TopSpace; :: thesis: for A, B being Subset of T holds
( A \/ B = [#] T iff A ` c= B )
let A, B be Subset of T; :: thesis: ( A \/ B = [#] T iff A ` c= B )

A1: now

assume A \/ B = [#] T ; :: thesis: A ` c= B
then ([#] T) \ A = B \ A by XBOOLE_1:40;
hence A ` c= B by XBOOLE_1:36; :: thesis: verum

end;

now

assume A ` c= B ; :: thesis: A \/ B = [#] T
then A \/ (A ` ) c= A \/ B by XBOOLE_1:9;
then ( [#] T c= A \/ B & A \/ B c= [#] T ) by PRE_TOPC:18;
hence A \/ B = [#] T by XBOOLE_0:def 10; :: thesis: verum

end;

hence ( A \/ B = [#] T iff A ` c= B ) by A1; :: thesis: verum