let X be non empty set ; :: thesis: for A, B being non empty Subset of X st A c< B holds
ex p being Element of X st
( p in B & A c= B \ {p} )
let A, B be non empty Subset of X; :: thesis: ( A c< B implies ex p being Element of X st
( p in B & A c= B \ {p} ) )
assume A1: A c< B ; :: thesis: ex p being Element of X st
( p in B & A c= B \ {p} )
then B \ A <> {} by XBOOLE_1:105;
then consider p being set such that
A2: p in B \ A by XBOOLE_0:def 1;
A3: ( p in B & not p in A ) by A2, XBOOLE_0:def 5;
reconsider p = p as Element of X by A2;
take p ; :: thesis: ( p in B & A c= B \ {p} )
A c= B by A1, XBOOLE_0:def 8;
hence ( p in B & A c= B \ {p} ) by A3, ZFMISC_1:40; :: thesis: verum