let R be non empty transitive asymmetric RelStr ; :: thesis: for a being bag of the carrier of R st a <> EmptyBag the carrier of R holds
{ x where x is Element of R : x is_maximal_in support a } <> {}
let a be bag of the carrier of R; :: thesis: ( a <> EmptyBag the carrier of R implies { x where x is Element of R : x is_maximal_in support a } <> {} )
set I = the carrier of R;
given x being Element of R such that A1: a . x <> (EmptyBag the carrier of R) . x ; :: according to PBOOLE:def 21 :: thesis: { x where x is Element of R : x is_maximal_in support a } <> {}
(EmptyBag the carrier of R) . x = 0 by FUNCOP_1:7;
then x in support a by A1, PRE_POLY:def 7;
then consider x being Element of R such that
A2: x is_maximal_in support a by Th12;
x in { y where y is Element of R : y is_maximal_in support a } by A2;
hence { x where x is Element of R : x is_maximal_in support a } <> {} ; :: thesis: verum