let X be non empty set ; :: thesis: for B being empty Subset-Family of X st ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B holds
FinMeetCl B c= UniCl B
let B be empty Subset-Family of X; :: thesis: ( ( for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB ) & X = union B implies FinMeetCl B c= UniCl B )
assume that
for B1, B2 being Element of B ex BB being Subset of B st B1 /\ B2 = union BB and
A1: X = union B ; :: thesis: FinMeetCl B c= UniCl B
FinMeetCl B c= UniCl B

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in FinMeetCl B or x in UniCl B )
assume A2: x in FinMeetCl B ; :: thesis: x in UniCl B
then reconsider x1 = x as Subset of X ;
consider Y being Subset-Family of X such that
A3: Y c= B and
Y is finite and
A4: x1 = Intersect Y by A2, CANTOR_1:def 3;
( Y = {} & meet {} = {} ) by A3, SETFAM_1:1;
then x1 = X by A4, SETFAM_1:def 9;
hence x in UniCl B by A1, CANTOR_1:def 1; :: thesis: verum

end;

hence FinMeetCl B c= UniCl B ; :: thesis: verum