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

proof

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in (x "/\" ) " {x} or q in uparrow x )
assume A1: q in (x "/\" ) " {x} ; :: thesis: q in uparrow x
then reconsider q1 = q as Element of L ;
A2: (x "/\" ) . q1 in {x} by A1, FUNCT_1:def 13;
x "/\" q1 = (x "/\" ) . q1 by WAYBEL_1:def 18
.= x by A2, TARSKI:def 1 ;
then x <= q1 by YELLOW_0:25;
hence q in uparrow x by WAYBEL_0:18; :: thesis: verum

end;

let q be set ; :: according to TARSKI:def 3 :: thesis: ( not q in uparrow x or q in (x "/\" ) " {x} )
assume A3: q in uparrow x ; :: thesis: q in (x "/\" ) " {x}
then reconsider q1 = q as Element of L ;
A4: x <= q1 by A3, WAYBEL_0:18;
(x "/\" ) . q1 = x "/\" q1 by WAYBEL_1:def 18
.= x by A4, YELLOW_0:25 ;
then ( dom (x "/\" ) = the carrier of L & (x "/\" ) . q1 in {x} ) by FUNCT_2:def 1, TARSKI:def 1;
hence q in (x "/\" ) " {x} by FUNCT_1:def 13; :: thesis: verum