let L be reflexive antisymmetric with_infima RelStr ; :: thesis: for x being Element of L holds uparrow x = { z where z is Element of L : z "/\" x = x }
let x be Element of L; :: thesis: uparrow x = { z where z is Element of L : z "/\" x = x }
thus uparrow x c= { z where z is Element of L : z "/\" x = x } :: according to XBOOLE_0:def 10 :: thesis: { z where z is Element of L : z "/\" x = x } c= uparrow x

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in uparrow x or q in { z where z is Element of L : z "/\" x = x } )
assume A1: q in uparrow x ; :: thesis: q in { z where z is Element of L : z "/\" x = x }
then reconsider q1 = q as Element of L ;
x <= q1 by A1, WAYBEL_0:18;
then q1 "/\" x = x by YELLOW_0:25;
hence q in { z where z is Element of L : z "/\" x = x } ; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in { z where z is Element of L : z "/\" x = x } or q in uparrow x )
assume q in { z where z is Element of L : z "/\" x = x } ; :: thesis: q in uparrow x
then consider z being Element of L such that
A2: q = z and
A3: z "/\" x = x ;
x <= z by A3, YELLOW_0:25;
hence q in uparrow x by A2, WAYBEL_0:18; :: thesis: verum