let L be Lattice; :: thesis: (.L.> is prime
set F = (.L.>;
for p, q being Element of L holds
( p "/\" q in (.L.> iff ( p in (.L.> or q in (.L.> ) ) ;
hence (.L.> is prime by FILTER_2:def 10; :: thesis: verum