let L be non empty reflexive transitive RelStr ; :: thesis: ( ( for x being Element of L
for N being net of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ) implies L is satisfying_MC )
assume A1: for x being Element of L
for N being net of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) ; :: thesis: L is satisfying_MC
let x be Element of L; :: according to WAYBEL_2:def 6 :: thesis: for b₁ being Element of K10( the carrier of L) holds x "/\" ("\/" (b₁,L)) = "\/" (({x} "/\" b₁),L)
let D be non empty directed Subset of L; :: thesis: x "/\" ("\/" (D,L)) = "\/" (({x} "/\" D),L)
reconsider n = id D as Function of D, the carrier of L by FUNCT_2:7;
set N = NetStr(# D,( the InternalRel of L |_2 D),n #);
A2: ( NetStr(# D,( the InternalRel of L |_2 D),n #) is eventually-directed & Sup = sup NetStr(# D,( the InternalRel of L |_2 D),n #) ) by WAYBEL_2:20;
D c= D ;
then A3: D = n .: D by FUNCT_1:92
.= rng (netmap (NetStr(# D,( the InternalRel of L |_2 D),n #),L)) by RELSET_1:22 ;
hence x "/\" (sup D) = x "/\" (Sup ) by YELLOW_2:def 5
.= sup ({x} "/\" D) by A1, A3, A2 ;
:: thesis: verum