let L be non empty RelStr ; :: thesis: for a being Element of L
for N being net of L holds a "/\" N is net of L
let a be Element of L; :: thesis: for N being net of L holds a "/\" N is net of L
let N be net of L; :: thesis: a "/\" N is net of L
set aN = a "/\" N;
a "/\" N is transitive
proof
let x, y, z be Element of (a "/\" N); :: according to YELLOW_0:def 2 :: thesis: ( not x <= y or not y <= z or x <= z )
assume A1: ( x <= y & y <= z ) ; :: thesis: x <= z
reconsider x1 = x, y1 = y, z1 = z as Element of N by WAYBEL_2:22;
A2: RelStr(# the carrier of N, the InternalRel of N #) = RelStr(# the carrier of (a "/\" N), the InternalRel of (a "/\" N) #) by WAYBEL_2:def 3;
then ( x1 <= y1 & y1 <= z1 ) by A1;
then x1 <= z1 by YELLOW_0:def 2;
hence x <= z by A2; :: thesis: verum
end;
hence a "/\" N is net of L ; :: thesis: verum