let TS be TopStruct ; :: thesis: for A, B being Subset of TS st A <> B holds
A ` <> B `
let A, B be Subset of TS; :: thesis: ( A <> B implies A ` <> B ` )
assume A1: A <> B ; :: thesis: A ` <> B `
assume A ` = B ` ; :: thesis: contradiction
then A = (B `) ` ;
hence contradiction by A1; :: thesis: verum