let E be set ; :: thesis: for A, B, C being Subset of E st A c= B & C misses B holds
A c= C `
let A, B, C be Subset of E; :: thesis: ( A c= B & C misses B implies A c= C ` )
assume ( A c= B & C misses B ) ; :: thesis: A c= C `
then A misses C by XBOOLE_1:63;
hence A c= C ` by Th23; :: thesis: verum