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

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

hence
FinMeetCl B c= UniCl B
; :: thesis: verum
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;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