let L be non empty RelStr ; :: thesis: for x, y being Element of L st x is_minimal_in the carrier of L \ (downarrow y) holds
(downarrow x) \ {x} = (downarrow x) /\ (downarrow y)
let x, y be Element of L; :: thesis: ( x is_minimal_in the carrier of L \ (downarrow y) implies (downarrow x) \ {x} = (downarrow x) /\ (downarrow y) )
assume A1: x is_minimal_in the carrier of L \ (downarrow y) ; :: thesis: (downarrow x) \ {x} = (downarrow x) /\ (downarrow y)
then x in the carrier of L \ (downarrow y) by WAYBEL_4:57;
then not x in downarrow y by XBOOLE_0:def 5;
then A2: not x <= y by WAYBEL_0:17;
thus (downarrow x) \ {x} c= (downarrow x) /\ (downarrow y) :: according to XBOOLE_0:def 10 :: thesis: (downarrow x) /\ (downarrow y) c= (downarrow x) \ {x}

proof

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (downarrow x) \ {x} or a in (downarrow x) /\ (downarrow y) )
assume A3: a in (downarrow x) \ {x} ; :: thesis: a in (downarrow x) /\ (downarrow y)
then A4: ( a in downarrow x & not a in {x} ) by XBOOLE_0:def 5;
reconsider a1 = a as Element of L by A3;
( a1 <= x & a1 <> x ) by A4, TARSKI:def 1, WAYBEL_0:17;
then a1 < x by ORDERS_2:def 10;
then not a1 in the carrier of L \ (downarrow y) by A1, WAYBEL_4:57;
then a in downarrow y by XBOOLE_0:def 5;
hence a in (downarrow x) /\ (downarrow y) by A4, XBOOLE_0:def 4; :: thesis: verum

end;

let a be set ; :: according to TARSKI:def 3 :: thesis: ( not a in (downarrow x) /\ (downarrow y) or a in (downarrow x) \ {x} )
assume A5: a in (downarrow x) /\ (downarrow y) ; :: thesis: a in (downarrow x) \ {x}
then A6: ( a in downarrow x & a in downarrow y ) by XBOOLE_0:def 4;
reconsider a1 = a as Element of L by A5;
a1 <= y by A6, WAYBEL_0:17;
then not a in {x} by A2, TARSKI:def 1;
hence a in (downarrow x) \ {x} by A6, XBOOLE_0:def 5; :: thesis: verum