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 \/ H c= <.(F \/ H).) by FILTER_0:def 4;
( F c= F \/ H & H c= F \/ H ) by XBOOLE_1:7;
hence ( F c= <.(F \/ H).) & H c= <.(F \/ H).) ) by A1; :: thesis: verum