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 object ; :: according to TARSKI:def 3 :: thesis: ( not x in bool A or x in bool B )
reconsider xx = x as set by TARSKI:1;
assume x in bool A ; :: thesis: x in bool B
then xx c= A by Def1;
then xx c= B by A1;
hence x in bool B by Def1; :: thesis: verum