let T be TopStruct ; :: thesis: for M being Subset of T
for F being Subset-Family of T st M c= union F holds
M = union (F | M)
let M be Subset of T; :: thesis: for F being Subset-Family of T st M c= union F holds
M = union (F | M)
let F be Subset-Family of T; :: thesis: ( M c= union F implies M = union (F | M) )
assume A1: M c= union F ; :: thesis: M = union (F | M)
for x being object holds
( x in M iff x in union (F | M) )

proof

let x be object ; :: thesis: ( x in M iff x in union (F | M) )

hereby :: thesis: ( x in union (F | M) implies x in M )

assume A2: x in M ; :: thesis: x in union (F | M)
then consider A being set such that
A3: x in A and
A4: A in F by A1, TARSKI:def 4;
reconsider A9 = A as Subset of T by A4;
A /\ M c= M by XBOOLE_1:17;
then A /\ M c= [#] (T | M) by PRE_TOPC:def 5;
then reconsider B = A9 /\ M as Subset of (T | M) ;
A5: B in F | M by A4, Def3;
x in A /\ M by A2, A3, XBOOLE_0:def 4;
hence x in union (F | M) by A5, TARSKI:def 4; :: thesis: verum

end;

assume x in union (F | M) ; :: thesis: x in M
then consider A being set such that
A6: x in A and
A7: A in F | M by TARSKI:def 4;
reconsider B = A as Subset of (T | M) by A7;
ex R being Subset of T st
( R in F & R /\ M = B ) by A7, Def3;
hence x in M by A6, XBOOLE_0:def 4; :: thesis: verum

end;

hence M = union (F | M) by TARSKI:2; :: thesis: verum