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:56;
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 object ; :: 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 reconsider a1 = a as Element of L ;
not a in {x} by A3, XBOOLE_0:def 5;
then A4: a1 <> x by TARSKI:def 1;
A5: a in downarrow x by A3, XBOOLE_0:def 5;
then a1 <= x by WAYBEL_0:17;
then a1 < x by A4, ORDERS_2:def 6;
then not a1 in the carrier of L \ (downarrow y) by A1, WAYBEL_4:56;
then a in downarrow y by XBOOLE_0:def 5;
hence a in (downarrow x) /\ (downarrow y) by A5, XBOOLE_0:def 4; :: thesis: verum

end;

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