let X be TopSpace; :: thesis: for A1, A2 being Subset of X st A1 misses A2 & A1 is open holds
A1 misses Cl A2
let A1, A2 be Subset of X; :: thesis: ( A1 misses A2 & A1 is open implies A1 misses Cl A2 )
assume A1: A1 misses A2 ; :: thesis: ( not A1 is open or A1 misses Cl A2 )
thus ( A1 is open implies A1 misses Cl A2 ) :: thesis: verum
proof
assume A2: A1 is open ; :: thesis: A1 misses Cl A2
A2 c= A1 ` by A1, SUBSET_1:23;
then Cl A2 c= A1 ` by A2, TOPS_1:5;
then Cl A2 misses (A1 `) ` by SUBSET_1:24;
hence A1 misses Cl A2 ; :: thesis: verum
end;