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

proof

let x be object ; :: 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 and
A2: p in F and
A3: q in H ;
H c= F \/ H by XBOOLE_1:7;
then A4: q in F \/ H by A3;
A5: F \/ H c= <.(F \/ H).) by Def4;
F c= F \/ H by XBOOLE_1:7;
then p in F \/ H by A2;
hence x in <.(F \/ H).) by A1, A4, A5, Th9; :: thesis: verum

end;

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