let X, Y be set ; :: thesis: ( X c< Y implies ex x being object st
( x in Y & X c= Y \ {x} ) )
assume A1: X c< Y ; :: thesis: ex x being object st
( x in Y & X c= Y \ {x} )
then consider x being object such that
A2: x in Y and
A3: not x in X by Th6;
take x ; :: thesis: ( x in Y & X c= Y \ {x} )
thus x in Y by A2; :: thesis: X c= Y \ {x}
let y be object ; :: according to TARSKI:def 3 :: thesis: ( y nin X or not y nin Y \ {x} )
assume A4: y in X ; :: thesis: not y nin Y \ {x}
then y <> x by A3;
then A5: not y in {x} by TARSKI:def 1;
X c= Y by A1;
then y in Y by A4;
hence not y nin Y \ {x} by Def5, A5; :: thesis: verum