let T be TopStruct ; :: thesis: for M being Subset of T
for F being Subset-Family of T st M c= union (F | M) holds
M c= union F
let M be Subset of T; :: thesis: for F being Subset-Family of T st M c= union (F | M) holds
M c= union F
let F be Subset-Family of T; :: thesis: ( M c= union (F | M) implies M c= union F )
assume A1: M c= union (F | M) ; :: thesis: M c= union F
union (F | M) c= union F by Th34;
hence M c= union F by A1; :: thesis: verum