let X be non empty set ; :: thesis: for x, y being set st x c= y holds
{ t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z }
let x, y be set ; :: thesis: ( x c= y implies { t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z } )
assume A1: x c= y ; :: thesis: { t where t is Element of X : y c= t } c= { z where z is Element of X : x c= z }
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in { t where t is Element of X : y c= t } or a in { z where z is Element of X : x c= z } )
reconsider aa = a as set by TARSKI:1;
assume a in { t where t is Element of X : y c= t } ; :: thesis: a in { z where z is Element of X : x c= z }
then A2: ex b being Element of X st
( b = a & y c= b ) ;
then x c= aa by A1;
hence a in { z where z is Element of X : x c= z } by A2; :: thesis: verum