let A, B be set ; :: thesis: ( A c= B implies bool A c= bool B )
assume A1: A c= B ; :: thesis: bool A c= bool B
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in bool A or x in bool B )
assume x in bool A ; :: thesis: x in bool B
then x c= A by Def1;
then x c= B by A1, XBOOLE_1:1;
hence x in bool B by Def1; :: thesis: verum