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 )

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

( 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 A4:
I = uparrow x
; :: thesis: I is principal
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;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

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