let L be Lattice; :: thesis: for F, H being Filter of L holds
( F c= <.(F \/ H).) & H c= <.(F \/ H).) )
let F, H be Filter of L; :: thesis: ( F c= <.(F \/ H).) & H c= <.(F \/ H).) )
A1: ( F c= F \/ H & H c= F \/ H ) by XBOOLE_1:7;
F \/ H c= <.(F \/ H).) by FILTER_0:def 5;
hence ( F c= <.(F \/ H).) & H c= <.(F \/ H).) ) by A1, XBOOLE_1:1; :: thesis: verum