let D be set ; :: thesis: for F being Subset-Family of D st F <> {} holds
union () = ([#] D) \ (meet F)

let F be Subset-Family of D; :: thesis: ( F <> {} implies union () = ([#] D) \ (meet F) )
assume A1: F <> {} ; :: thesis: union () = ([#] D) \ (meet F)
A2: ([#] D) \ (meet F) c= union ()
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in ([#] D) \ (meet F) or x in union () )
assume A3: x in ([#] D) \ (meet F) ; :: thesis: x in union ()
then not x in meet F by XBOOLE_0:def 5;
then consider X being set such that
A4: X in F and
A5: not x in X by ;
reconsider X = X as Subset of D by A4;
reconsider XX = X ` as set ;
A6: (X `) ` = X ;
ex Y being set st
( x in Y & Y in COMPLEMENT F )
proof
take XX ; :: thesis: ( x in XX & XX in COMPLEMENT F )
thus ( x in XX & XX in COMPLEMENT F ) by ; :: thesis: verum
end;
hence x in union () by TARSKI:def 4; :: thesis: verum
end;
union () c= ([#] D) \ (meet F)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union () or x in ([#] D) \ (meet F) )
assume A7: x in union () ; :: thesis: x in ([#] D) \ (meet F)
then consider X being set such that
A8: x in X and
A9: X in COMPLEMENT F by TARSKI:def 4;
reconsider X = X as Subset of D by A9;
reconsider XX = X ` as set ;
ex Y being set st
( Y in F & not x in Y )
proof
take Y = XX; :: thesis: ( Y in F & not x in Y )
thus Y in F by ; :: thesis: not x in Y
thus not x in Y by ; :: thesis: verum
end;
then not x in meet F by Def1;
hence x in ([#] D) \ (meet F) by ; :: thesis: verum
end;
hence union () = ([#] D) \ (meet F) by A2; :: thesis: verum