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

proof

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in (y "/\") .: (uparrow y) or q in {y} )
assume q in (y "/\") .: (uparrow y) ; :: thesis: q in {y}
then consider a being object such that
a in dom (y "/\") and
A1: a in uparrow y and
A2: q = (y "/\") . a by FUNCT_1:def 6;
reconsider a = a as Element of L by A1;
A3: y <= a by A1, WAYBEL_0:18;
q = y "/\" a by A2, WAYBEL_1:def 18
.= y by A3, YELLOW_0:25 ;
hence q in {y} by TARSKI:def 1; :: thesis: verum

end;

let q be object ; :: according to TARSKI:def 3 :: thesis: ( not q in {y} or q in (y "/\") .: (uparrow y) )
assume q in {y} ; :: thesis: q in (y "/\") .: (uparrow y)
then A4: q = y by TARSKI:def 1;
y <= y ;
then A5: ( dom (y "/\") = the carrier of L & y in uparrow y ) by FUNCT_2:def 1, WAYBEL_0:18;
y = y "/\" y by YELLOW_0:25
.= (y "/\") . y by WAYBEL_1:def 18 ;
hence q in (y "/\") .: (uparrow y) by A4, A5, FUNCT_1:def 6; :: thesis: verum