let L be Lattice; :: thesis: for F being Filter of L holds
( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
let F be Filter of L; :: thesis: ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F )
ex o1, o2 being BinOp of F st
( o1 = the L_join of L || F & o2 = the L_meet of L || F & latt F = LattStr(# F,o1,o2 #) ) by Def9;
hence ( the carrier of (latt F) = F & the L_join of (latt F) = the L_join of L || F & the L_meet of (latt F) = the L_meet of L || F ) ; :: thesis: verum