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:9;
reconsider N = NetStr(# D,(the InternalRel of L |_2 D),n #) as prenet of L by Th19;
D c= D ;
then A2: D = n .: D by FUNCT_1:162
.= rng (netmap N,L) by FUNCT_2:45 ;
A3: Sup = sup N ;
thus x "/\" (sup D) = x "/\" (Sup ) by A2, YELLOW_2:def 5
.= sup ({x} "/\" D) by A1, A2, A3, Th20 ; :: thesis: verum