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 )
per cases ( S = {} or S <> {} ) ;
suppose A3: S = {} ; :: thesis: ( not sup ((meet S) /\ C) = C or C in meet S )
not sup ((meet S) /\ C) = C
proof
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;
hence ( not sup ((meet S) /\ C) = C or C in meet S ) ; :: thesis: verum
end;
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
proof
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;
hence C in meet S by A5, SETFAM_1:def 1; :: thesis: verum
end;
end;