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 consider p being Element of X such that
A2: p in B \ A by Th4, XBOOLE_1:105;
A3: not p in A by A2, XBOOLE_0:def 5;
take p ; :: thesis: ( p in B & A c= B \ {p} )
thus ( p in B & A c= B \ {p} ) by A1, A2, A3, XBOOLE_0:def 5, ZFMISC_1:34; :: thesis: verum