let L be Lattice; :: thesis: for F, H being Filter of L holds <.(F \/ H).) = <.(F "/\" H).)
let F, H be Filter of L; :: thesis: <.(F \/ H).) = <.(F "/\" H).)
( F c= F "/\" H & H c= F "/\" H ) by Th49;
then F \/ H c= F "/\" H by XBOOLE_1:8;
hence <.(F \/ H).) c= <.(F "/\" H).) by Th27; :: according to XBOOLE_0:def 10 :: thesis: <.(F "/\" H).) c= <.(F \/ H).)
F "/\" H c= <.(F \/ H).)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F "/\" H or x in <.(F \/ H).) )
assume x in F "/\" H ; :: thesis: x in <.(F \/ H).)
then consider p, q being Element of L such that
A1: ( x = p "/\" q & p in F & q in H ) ;
( F c= F \/ H & H c= F \/ H ) by XBOOLE_1:7;
then ( p in F \/ H & q in F \/ H & F \/ H c= <.(F \/ H).) & F \/ H c= <.(F \/ H).) ) by A1, Def5;
hence x in <.(F \/ H).) by A1, Th9; :: thesis: verum

end;

then <.(F "/\" H).) c= <.<.(F \/ H).).) by Th27;
hence <.(F "/\" H).) c= <.(F \/ H).) by Th26; :: thesis: verum