let X be non empty set ; :: thesis: for F1, F2 being Filter of X st ( for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty ) holds
ex F being Filter of X st
( F is_filter-finer_than F1 & F is_filter-finer_than F2 )
let F1, F2 be Filter of X; :: thesis: ( ( for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty ) implies ex F being Filter of X st
( F is_filter-finer_than F1 & F is_filter-finer_than F2 ) )
assume A1: for M1 being Element of F1
for M2 being Element of F2 holds not M1 /\ M2 is empty ; :: thesis: ex F being Filter of X st
( F is_filter-finer_than F1 & F is_filter-finer_than F2 )
set F = { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } ;
take { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } ; :: thesis: ( { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is Element of bool (bool X) & { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is Filter of X & { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is_filter-finer_than F1 & { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is_filter-finer_than F2 )
{ (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is non empty Subset-Family of X
proof
set M1 = the Element of F1;
set M2 = the Element of F2;
A2: the Element of F1 /\ the Element of F2 in { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } ;
{ (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } c= bool X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } or x in bool X )
assume x in { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } ; :: thesis: x in bool X
then consider M1 being Element of F1, M2 being Element of F2 such that
A3: x = M1 /\ M2 ;
thus x in bool X by A3; :: thesis: verum
end;
hence { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is non empty Subset-Family of X by A2; :: thesis: verum
end;
then reconsider F = { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } as non empty Subset-Family of X ;
now :: thesis: ( ( {} in F implies not {} in F ) & ( for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) ) ) )
hereby :: thesis: for Y1, Y2 being Subset of X holds
( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) )
assume {} in F ; :: thesis: not {} in F
then consider M1 being Element of F1, M2 being Element of F2 such that
A4: {} = M1 /\ M2 ;
thus not {} in F by A4, A1; :: thesis: verum
end;
hereby :: thesis: verum
let Y1, Y2 be Subset of X; :: thesis: ( ( Y1 in F & Y2 in F implies Y1 /\ Y2 in F ) & ( Y1 in F & Y1 c= Y2 implies Y2 in F ) )
hereby :: thesis: ( Y1 in F & Y1 c= Y2 implies Y2 in F )
assume that
A5: Y1 in F and
A6: Y2 in F ; :: thesis: Y1 /\ Y2 in F
consider M1 being Element of F1, M2 being Element of F2 such that
A7: Y1 = M1 /\ M2 by A5;
consider M3 being Element of F1, M4 being Element of F2 such that
A8: Y2 = M3 /\ M4 by A6;
Y1 /\ Y2 = M1 /\ (M2 /\ (M3 /\ M4)) by A7, A8, XBOOLE_1:16;
then Y1 /\ Y2 = M1 /\ (M3 /\ (M4 /\ M2)) by XBOOLE_1:16;
then A9: Y1 /\ Y2 = (M1 /\ M3) /\ (M2 /\ M4) by XBOOLE_1:16;
( M1 /\ M3 is Element of F1 & M2 /\ M4 is Element of F2 ) by CARD_FIL:def 1;
hence Y1 /\ Y2 in F by A9; :: thesis: verum
end;
assume that
A10: Y1 in F and
A11: Y1 c= Y2 ; :: thesis: Y2 in F
consider M1 being Element of F1, M2 being Element of F2 such that
A12: Y1 = M1 /\ M2 by A10;
Y2 \/ (M1 /\ M2) = Y2 by A11, A12, XBOOLE_1:12;
then A13: Y2 = (M1 \/ Y2) /\ (M2 \/ Y2) by XBOOLE_1:24;
( M1 c= M1 \/ Y2 & M2 c= M2 \/ Y2 ) by XBOOLE_1:7;
then ( M1 \/ Y2 is Element of F1 & M2 \/ Y2 is Element of F2 ) by CARD_FIL:def 1;
hence Y2 in F by A13; :: thesis: verum
end;
end;
then reconsider F0 = F as Filter of X by CARD_FIL:def 1;
A14: ( X in F1 & X in F2 ) by CARD_FIL:5;
F1 c= F0
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F1 or x in F0 )
assume A15: x in F1 ; :: thesis: x in F0
then reconsider x = x as Subset of X ;
x = x /\ X by XBOOLE_1:17, XBOOLE_1:19;
hence x in F0 by A14, A15; :: thesis: verum
end;
then A16: F0 is_filter-finer_than F1 ;
F2 c= F0
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F2 or x in F0 )
assume A17: x in F2 ; :: thesis: x in F0
then reconsider x = x as Subset of X ;
x = x /\ X by XBOOLE_1:17, XBOOLE_1:19;
hence x in F0 by A14, A17; :: thesis: verum
end;
then F0 is_filter-finer_than F2 ;
hence ( { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is Element of bool (bool X) & { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is Filter of X & { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is_filter-finer_than F1 & { (M1 /\ M2) where M1 is Element of F1, M2 is Element of F2 : verum } is_filter-finer_than F2 ) by A16; :: thesis: verum