let L be non empty RelStr ; :: thesis: for x being Element of L
for X being Subset of L holds
( X c= uparrow x iff x is_<=_than X )
let x be Element of L; :: thesis: for X being Subset of L holds
( X c= uparrow x iff x is_<=_than X )
let X be Subset of L; :: thesis: ( X c= uparrow x iff x is_<=_than X )

hereby :: thesis: ( x is_<=_than X implies X c= uparrow x )

assume A1: X c= uparrow x ; :: thesis: x is_<=_than X
thus x is_<=_than X :: thesis: verum

proof

let a be Element of L; :: according to LATTICE3:def 8 :: thesis: ( not a in X or x <= a )
assume a in X ; :: thesis: x <= a
hence x <= a by A1, WAYBEL_0:18; :: thesis: verum

end;

end;

assume A2: for a being Element of L st a in X holds
x <= a ; :: according to LATTICE3:def 8 :: thesis: X c= uparrow x
let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in X or a in uparrow x )
assume A3: a in X ; :: thesis: a in uparrow x
then reconsider a = a as Element of L ;
x <= a by A2, A3;
hence a in uparrow x by WAYBEL_0:18; :: thesis: verum