let L be reflexive antisymmetric with_suprema RelStr ; :: thesis: for x being Element of L holds downarrow x = { z where z is Element of L : z "\/" x = x }
let x be Element of L; :: thesis: downarrow x = { z where z is Element of L : z "\/" x = x }
thus downarrow 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= downarrow x
proof
let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in downarrow x or q in { z where z is Element of L : z "\/" x = x } )
assume A1: q in downarrow 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:17;
then q1 "\/" x = x by YELLOW_0:24;
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 downarrow x )
assume q in { z where z is Element of L : z "\/" x = x } ; :: thesis: q in downarrow x
then consider z being Element of L such that
A2: q = z and
A3: z "\/" x = x ;
x >= z by A3, YELLOW_0:24;
hence q in downarrow x by A2, WAYBEL_0:17; :: thesis: verum