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

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

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

proof

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

end;

end;

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