let T be TopStruct ; :: thesis: for x, y being Point of T
for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) holds
Cl X c= Cl Y
let x, y be Point of T; :: thesis: for X, Y being Subset of T st X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) holds
Cl X c= Cl Y
let X, Y be Subset of T; :: thesis: ( X = {x} & Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) implies Cl X c= Cl Y )
assume that
A1: X = {x} and
A2: ( Y = {y} & ( for V being Subset of T st V is open & x in V holds
y in V ) ) ; :: thesis: Cl X c= Cl Y
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Cl X or z in Cl Y )
assume A3: z in Cl X ; :: thesis: z in Cl Y
for V being Subset of T st V is open & z in V holds
Y meets V

proof

let V be Subset of T; :: thesis: ( V is open & z in V implies Y meets V )
assume that
A4: V is open and
A5: z in V ; :: thesis: Y meets V
X meets V by A3, A4, A5, PRE_TOPC:def 7;
then x in V by A1, ZFMISC_1:50;
hence Y meets V by A2, A4, ZFMISC_1:48; :: thesis: verum

end;

hence z in Cl Y by A3, PRE_TOPC:def 7; :: thesis: verum