let L be non empty reflexive RelStr ; :: thesis: ( ( for x being Element of L

for N being prenet 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 prenet 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 D being non empty directed Subset of L holds x "/\" (sup D) = sup ({x} "/\" D)

let D be non empty directed Subset of L; :: thesis: x "/\" (sup D) = sup ({x} "/\" D)

reconsider n = id D as Function of D, the carrier of L by FUNCT_2:7;

reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as prenet of L by Th19;

A2: Sup = sup N ;

D c= D ;

then A3: D = n .: D by FUNCT_1:92

.= rng (netmap (N,L)) by RELSET_1:22 ;

hence x "/\" (sup D) = x "/\" (Sup ) by YELLOW_2:def 5

.= sup ({x} "/\" D) by A1, A3, A2, Th20 ;

:: thesis: verum

for N being prenet 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 prenet 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 D being non empty directed Subset of L holds x "/\" (sup D) = sup ({x} "/\" D)

let D be non empty directed Subset of L; :: thesis: x "/\" (sup D) = sup ({x} "/\" D)

reconsider n = id D as Function of D, the carrier of L by FUNCT_2:7;

reconsider N = NetStr(# D,( the InternalRel of L |_2 D),n #) as prenet of L by Th19;

A2: Sup = sup N ;

D c= D ;

then A3: D = n .: D by FUNCT_1:92

.= rng (netmap (N,L)) by RELSET_1:22 ;

hence x "/\" (sup D) = x "/\" (Sup ) by YELLOW_2:def 5

.= sup ({x} "/\" D) by A1, A3, A2, Th20 ;

:: thesis: verum