let X be non empty TopSpace; :: thesis: for Y0 being non empty SubSpace of X
for C, A being Subset of X
for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let Y0 be non empty SubSpace of X; :: thesis: for C, A being Subset of X
for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let C, A be Subset of X; :: thesis: for B being Subset of Y0 st C is open & C c= the carrier of Y0 & A c= C & A = B holds
Int A = Int B
let B be Subset of Y0; :: thesis: ( C is open & C c= the carrier of Y0 & A c= C & A = B implies Int A = Int B )
assume A1: C is open ; :: thesis: ( not C c= the carrier of Y0 or not A c= C or not A = B or Int A = Int B )
assume A2: C c= the carrier of Y0 ; :: thesis: ( not A c= C or not A = B or Int A = Int B )
assume A3: A c= C ; :: thesis: ( not A = B or Int A = Int B )
assume A4: A = B ; :: thesis: Int A = Int B
A5: Int B c= B by TOPS_1:16;
then reconsider D = Int B as Subset of X by A4, XBOOLE_1:1;
Int B c= C by A3, A4, A5, XBOOLE_1:1;
then D is open by A1, A2, TSEP_1:9;
then A6: D c= Int A by A4, TOPS_1:16, TOPS_1:24;
Int A c= Int B by A4, Th56;
hence Int A = Int B by A6; :: thesis: verum