let M be non countable Aleph; :: thesis: for S being Subset-Family of M st ( for X being Element of S holds X is closed ) holds

meet S is closed

let S be Subset-Family of M; :: thesis: ( ( for X being Element of S holds X is closed ) implies meet S is closed )

assume A1: for X being Element of S holds X is closed ; :: thesis: meet S is closed

let C be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def 5 :: thesis: ( C in M & sup ((meet S) /\ C) = C implies C in meet S )

assume A2: C in M ; :: thesis: ( not sup ((meet S) /\ C) = C or C in meet S )

meet S is closed

let S be Subset-Family of M; :: thesis: ( ( for X being Element of S holds X is closed ) implies meet S is closed )

assume A1: for X being Element of S holds X is closed ; :: thesis: meet S is closed

let C be limit_ordinal infinite Ordinal; :: according to CARD_LAR:def 5 :: thesis: ( C in M & sup ((meet S) /\ C) = C implies C in meet S )

assume A2: C in M ; :: thesis: ( not sup ((meet S) /\ C) = C or C in meet S )

per cases
( S = {} or S <> {} )
;

end;

suppose A3:
S = {}
; :: thesis: ( not sup ((meet S) /\ C) = C or C in meet S )

not sup ((meet S) /\ C) = C

end;proof

hence
( not sup ((meet S) /\ C) = C or C in meet S )
; :: thesis: verum
assume A4:
sup ((meet S) /\ C) = C
; :: thesis: contradiction

meet S = {} by A3, SETFAM_1:def 1;

hence contradiction by A4, ORDINAL2:18; :: thesis: verum

end;meet S = {} by A3, SETFAM_1:def 1;

hence contradiction by A4, ORDINAL2:18; :: thesis: verum

suppose A5:
S <> {}
; :: thesis: ( not sup ((meet S) /\ C) = C or C in meet S )

assume A6:
sup ((meet S) /\ C) = C
; :: thesis: C in meet S

for X being set st X in S holds

C in X

end;for X being set st X in S holds

C in X

proof

hence
C in meet S
by A5, SETFAM_1:def 1; :: thesis: verum
let X be set ; :: thesis: ( X in S implies C in X )

assume A7: X in S ; :: thesis: C in X

reconsider X1 = X as Element of S by A7;

A8: X1 is closed by A1;

sup (X1 /\ C) c= sup C by ORDINAL2:22, XBOOLE_1:17;

then A9: sup (X1 /\ C) c= C by ORDINAL2:18;

(meet S) /\ C c= X1 /\ C by A7, SETFAM_1:3, XBOOLE_1:26;

then sup ((meet S) /\ C) c= sup (X1 /\ C) by ORDINAL2:22;

then sup (X1 /\ C) = C by A6, A9, XBOOLE_0:def 10;

hence C in X by A2, A8; :: thesis: verum

end;assume A7: X in S ; :: thesis: C in X

reconsider X1 = X as Element of S by A7;

A8: X1 is closed by A1;

sup (X1 /\ C) c= sup C by ORDINAL2:22, XBOOLE_1:17;

then A9: sup (X1 /\ C) c= C by ORDINAL2:18;

(meet S) /\ C c= X1 /\ C by A7, SETFAM_1:3, XBOOLE_1:26;

then sup ((meet S) /\ C) c= sup (X1 /\ C) by ORDINAL2:22;

then sup (X1 /\ C) = C by A6, A9, XBOOLE_0:def 10;

hence C in X by A2, A8; :: thesis: verum