let A, B be set ; :: thesis: ( A * c= B * implies A c= B )
assume A1: A * c= B * ; :: thesis: A c= B
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in B )
assume x in A ; :: thesis: x in B
then <*x*> in A * by Th18;
hence x in B by A1, Th18; :: thesis: verum