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 object ; :: 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 7;
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 object ; :: 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 7; :: thesis: verum