let E be set ; :: thesis: for A, B being Subset of E holds
( A misses B ` iff A c= B )
let A, B be Subset of E; :: thesis: ( A misses B ` iff A c= B )
(B `) ` = B ;
hence ( A misses B ` iff A c= B ) by Th23; :: thesis: verum