let L be reflexive antisymmetric with_suprema RelStr ; :: thesis: for x being Element of L holds uparrow x = {x} "\/" ([#] L)
let x be Element of L; :: thesis: uparrow x = {x} "\/" ([#] L)
A1: {x} "\/" ([#] L) = { (x "\/" s) where s is Element of L : s in [#] L } by YELLOW_4:15;
thus uparrow x c= {x} "\/" ([#] L) :: according to XBOOLE_0:def 10 :: thesis: {x} "\/" ([#] L) c= uparrow x
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in uparrow x or q in {x} "\/" ([#] L) )
assume A2: q in uparrow x ; :: thesis: q in {x} "\/" ([#] L)
then reconsider q1 = q as Element of L ;
x <= q1 by A2, WAYBEL_0:18;
then x "\/" q1 = q1 by YELLOW_0:24;
hence q in {x} "\/" ([#] L) by A1; :: thesis: verum
end;
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {x} "\/" ([#] L) or q in uparrow x )
assume q in {x} "\/" ([#] L) ; :: thesis: q in uparrow x
then consider z being Element of L such that
A3: q = x "\/" z and
z in [#] L by A1;
x <= x "\/" z by YELLOW_0:22;
hence q in uparrow x by A3, WAYBEL_0:18; :: thesis: verum