let L be non empty reflexive transitive RelStr ; :: thesis: for F being Filter of L holds
( F is principal iff ex x being Element of L st F = uparrow x )
let I be Filter of L; :: thesis: ( I is principal iff ex x being Element of L st I = uparrow x )
thus ( I is principal implies ex x being Element of L st I = uparrow x ) :: thesis: ( ex x being Element of L st I = uparrow x implies I is principal )
proof
given x being Element of L such that A1: x in I and
A2: x is_<=_than I ; :: according to WAYBEL_0:def 22 :: thesis: ex x being Element of L st I = uparrow x
take x ; :: thesis: I = uparrow x
thus I c= uparrow x by A2, Th18; :: according to XBOOLE_0:def 10 :: thesis: uparrow x c= I
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in uparrow x or z in I )
assume A3: z in uparrow x ; :: thesis: z in I
then reconsider z = z as Element of L ;
z >= x by A3, Th18;
hence z in I by A1, Def20; :: thesis: verum
end;
given x being Element of L such that A4: I = uparrow x ; :: thesis: I is principal
take x ; :: according to WAYBEL_0:def 22 :: thesis: ( x in I & x is_<=_than I )
x <= x ;
hence x in I by A4, Th18; :: thesis: x is_<=_than I
let y be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not y in I or x <= y )
thus ( not y in I or x <= y ) by A4, Th18; :: thesis: verum